/* mockturtle: C++ logic network library
 * Copyright (C) 2018-2019  EPFL
 *
 * Permission is hereby granted, free of charge, to any person
 * obtaining a copy of this software and associated documentation
 * files (the "Software"), to deal in the Software without
 * restriction, including without limitation the rights to use,
 * copy, modify, merge, publish, distribute, sublicense, and/or sell
 * copies of the Software, and to permit persons to whom the
 * Software is furnished to do so, subject to the following
 * conditions:
 *
 * The above copyright notice and this permission notice shall be
 * included in all copies or substantial portions of the Software.
 *
 * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
 * EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES
 * OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
 * NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT
 * HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY,
 * WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
 * FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR
 * OTHER DEALINGS IN THE SOFTWARE.
 */

/*!
  \file mig_npn.hpp
  \brief Replace with size-optimum MIGs from NPN

  \author Mathias Soeken
*/

#pragma once

#include <iostream>
#include <sstream>
#include <unordered_map>
#include <vector>

#include <kitty/dynamic_truth_table.hpp>
#include <kitty/npn.hpp>
#include <kitty/print.hpp>

#include "../../algorithms/cleanup.hpp"
#include "../../io/write_bench.hpp"
#include "../../networks/mig.hpp"
#include "../../traits.hpp"
#include "../../views/topo_view.hpp"

namespace mockturtle {

/*! \brief Resynthesis function based on pre-computed size-optimum MIGs.
 *
 * This resynthesis function can be passed to ``node_resynthesis``,
 * ``cut_rewriting``, and ``refactoring``.  It will produce an MIG based on
 * pre-computed size-optimum MIGs with up to at most 4 variables.
 * Consequently, the nodes' fan-in sizes in the input network must not exceed
 * 4.
 *
   \verbatim embed:rst

   Example

   .. code-block:: c++

      const klut_network klut = ...;
      mig_npn_resynthesis resyn;
      const auto mig = node_resynthesis<mig_network>( klut, resyn );
   \endverbatim
 */
class mig_npn_resynthesis {
  public:
    /*! \brief Default constructor.
     *
     * \param use_multiple If true, up to 10 structures are tried for each
     *                     function.
     */
    mig_npn_resynthesis(bool use_multiple = false) {
        if (use_multiple) {
            build_db10();
        } else {
            build_db();
        }
    }

    template <typename LeavesIterator, typename Fn>
    void operator()(mig_network& mig,
                    kitty::dynamic_truth_table const& function,
                    LeavesIterator begin, LeavesIterator end, Fn&& fn) {
        assert(function.num_vars() <= 4);
        const auto fe = kitty::extend_to(function, 4);
        const auto config = kitty::exact_npn_canonization(fe);

        const auto it = class2signal.find(
            static_cast<uint16_t>(std::get<0>(config)._bits[0]));

        std::vector<mig_network::signal> pis(4, mig.get_constant(false));
        std::copy(begin, end, pis.begin());

        std::vector<mig_network::signal> pis_perm(4);
        auto perm = std::get<2>(config);
        for (auto i = 0; i < 4; ++i) {
            pis_perm[i] = pis[perm[i]];
        }

        const auto& phase = std::get<1>(config);
        for (auto i = 0; i < 4; ++i) {
            if ((phase >> perm[i]) & 1) {
                pis_perm[i] = !pis_perm[i];
            }
        }

        for (auto const& po : it->second) {
            topo_view topo{db, po};
            auto f =
                cleanup_dangling(topo, mig, pis_perm.begin(), pis_perm.end())
                    .front();

            if (!fn(((phase >> 4) & 1) ? !f : f)) {
                return; /* quit */
            }
        }
    }

  private:
    void build_db() {
        std::vector<mig_network::signal> signals;
        signals.push_back(db.get_constant(false));

        auto p = nodes.begin();
        for (auto i = 0u; i < *p; ++i) {
            signals.push_back(db.create_pi());
        }

        p++;         /* point to number of outputs */
        p += *p + 1; /* move past number of output */

        /* create nodes */
        while (p != nodes.end()) {
            const auto c1 = signals[*p >> 1] ^ (*p & 1);
            ++p;
            const auto c2 = signals[*p >> 1] ^ (*p & 1);
            ++p;
            const auto c3 = signals[*p >> 1] ^ (*p & 1);
            ++p;

            signals.push_back(db.create_maj(c1, c2, c3));
        }

        /* create POs */
        p = nodes.begin() + 2;
        for (auto i = 0u; i < nodes[1]; ++i) {
            const auto driver = signals[*p >> 1] ^ (*p & 1);
            ++p;

            db.create_po(driver);
            class2signal[classes[i]].push_back(driver);
        }
    }

    void build_db10() {
        std::vector<mig_network::signal> signals;
        signals.push_back(db.get_constant(false));

        auto p = nodes10.begin();
        for (auto i = 0u; i < *p; ++i) {
            signals.push_back(db.create_pi());
        }

        p++; /* point to number of outputs */
        const auto num_functions = *p++;

        for (auto i = 0u; i < num_functions; ++i) {
            p += *p + 1;
        }

        /* create nodes */
        while (p != nodes10.end()) {
            const auto c1 = signals[*p >> 1] ^ (*p & 1);
            ++p;
            const auto c2 = signals[*p >> 1] ^ (*p & 1);
            ++p;
            const auto c3 = signals[*p >> 1] ^ (*p & 1);
            ++p;

            signals.push_back(db.create_maj(c1, c2, c3));
        }

        /* create PIs */
        p = nodes10.begin() + 2;
        for (auto i = 0u; i < nodes10[1]; ++i) {
            const auto functions = *p++;
            for (auto j = 0u; j < functions; ++j) {
                const auto driver = signals[*p >> 1] ^ (*p & 1);
                ++p;

                db.create_po(driver);
                class2signal[classes[i]].push_back(driver);
            }
        }
    }

    mig_network db;
    std::unordered_map<uint16_t, std::vector<mig_network::signal>> class2signal;

    inline static const std::vector<uint16_t> classes{
        {0x1ee1, 0x1be4, 0x1bd8, 0x18e7, 0x17e8, 0x17ac, 0x1798, 0x1796, 0x178e,
         0x177e, 0x16e9, 0x16bc, 0x169e, 0x003f, 0x0359, 0x0672, 0x07e9, 0x0693,
         0x0358, 0x01bf, 0x6996, 0x0356, 0x01bd, 0x001f, 0x01ac, 0x001e, 0x0676,
         0x01ab, 0x01aa, 0x001b, 0x07e1, 0x07e0, 0x0189, 0x03de, 0x035a, 0x1686,
         0x0186, 0x03db, 0x0357, 0x01be, 0x1683, 0x0368, 0x0183, 0x03d8, 0x07e6,
         0x0182, 0x03d7, 0x0181, 0x03d6, 0x167e, 0x016a, 0x007e, 0x0169, 0x006f,
         0x0069, 0x0168, 0x0001, 0x019a, 0x036b, 0x1697, 0x0369, 0x0199, 0x0000,
         0x169b, 0x003d, 0x036f, 0x0666, 0x019b, 0x0187, 0x03dc, 0x0667, 0x0003,
         0x168e, 0x06b6, 0x01eb, 0x07e2, 0x017e, 0x07b6, 0x007f, 0x19e3, 0x06b7,
         0x011a, 0x077e, 0x018b, 0x00ff, 0x0673, 0x01a8, 0x000f, 0x1696, 0x036a,
         0x011b, 0x0018, 0x0117, 0x1698, 0x036c, 0x01af, 0x0016, 0x067a, 0x0118,
         0x0017, 0x067b, 0x0119, 0x169a, 0x003c, 0x036e, 0x07e3, 0x017f, 0x03d4,
         0x06f0, 0x011e, 0x037c, 0x012c, 0x19e6, 0x01ef, 0x16a9, 0x037d, 0x006b,
         0x012d, 0x012f, 0x01fe, 0x0019, 0x03fc, 0x179a, 0x013c, 0x016b, 0x06f2,
         0x03c0, 0x033c, 0x1668, 0x0669, 0x019e, 0x013d, 0x0006, 0x019f, 0x013e,
         0x0776, 0x013f, 0x016e, 0x03c3, 0x3cc3, 0x033f, 0x166b, 0x016f, 0x011f,
         0x035e, 0x0690, 0x0180, 0x03d5, 0x06f1, 0x06b0, 0x037e, 0x03c1, 0x03c5,
         0x03c6, 0x01a9, 0x166e, 0x03cf, 0x03d9, 0x07bc, 0x01bc, 0x1681, 0x03dd,
         0x03c7, 0x06f9, 0x0660, 0x0196, 0x0661, 0x0197, 0x0662, 0x07f0, 0x0198,
         0x0663, 0x07f1, 0x0007, 0x066b, 0x033d, 0x1669, 0x066f, 0x01ad, 0x0678,
         0x01ae, 0x0679, 0x067e, 0x168b, 0x035f, 0x0691, 0x0696, 0x0697, 0x06b1,
         0x0778, 0x16ac, 0x06b2, 0x0779, 0x16ad, 0x01e8, 0x06b3, 0x0116, 0x077a,
         0x01e9, 0x06b4, 0x19e1, 0x01ea, 0x06b5, 0x01ee, 0x06b9, 0x06bd, 0x06f6,
         0x07b0, 0x07b1, 0x07b4, 0x07b5, 0x07f2, 0x07f8, 0x018f, 0x0ff0, 0x166a,
         0x035b, 0x1687, 0x1689, 0x036d, 0x069f, 0x1699}};
    inline static const std::vector<uint16_t> nodes{
        {4,    222,  17,   24,   34,   41,   46,   56,   68,   76,   84,   96,
         109,  116,  122,  127,  137,  142,  151,  157,  166,  173,  182,  188,
         193,  199,  208,  214,  220,  227,  232,  239,  247,  256,  259,  264,
         272,  278,  286,  293,  297,  300,  307,  312,  321,  328,  336,  344,
         351,  355,  362,  372,  378,  384,  387,  389,  393,  398,  401,  408,
         417,  421,  425,  433,  0,    439,  445,  451,  454,  459,  467,  472,
         475,  477,  482,  486,  491,  498,  502,  506,  509,  517,  523,  526,
         532,  537,  9,    545,  548,  335,  554,  560,  563,  568,  573,  576,
         580,  583,  586,  594,  596,  599,  603,  605,  612,  616,  622,  627,
         629,  630,  634,  638,  640,  644,  650,  657,  665,  669,  675,  677,
         679,  686,  691,  696,  702,  708,  713,  718,  722,  728,  738,  747,
         750,  755,  756,  761,  766,  770,  773,  778,  785,  789,  159,  797,
         801,  803,  810,  812,  820,  827,  831,  836,  844,  853,  857,  862,
         869,  876,  879,  887,  892,  900,  911,  915,  921,  927,  930,  938,
         941,  951,  954,  960,  966,  971,  975,  977,  985,  991,  1003, 1007,
         1011, 1014, 1020, 1027, 1030, 1037, 1039, 1041, 1044, 1049, 1053, 1060,
         1066, 1070, 1073, 1077, 1082, 1093, 1096, 1100, 1107, 1112, 1119, 1124,
         1135, 1138, 1141, 1147, 1148, 1152, 1159, 1166, 1175, 1178, 1186, 1191,
         1194, 1202, 1205, 1213, 1221, 1229, 1231, 1237, 1,    2,    4,    6,
         8,    11,   9,    10,   12,   7,    12,   14,   0,    2,    7,    8,
         10,   19,   8,    10,   21,   18,   20,   23,   5,    6,    8,    2,
         4,    6,    0,    26,   28,   1,    26,   28,   0,    31,   32,   6,
         9,    28,   8,    29,   36,   7,    36,   38,   0,    8,    28,   0,
         8,    43,   28,   43,   44,   0,    5,    8,    4,    7,    48,   0,
         2,    8,    2,    6,    48,   50,   53,   54,   0,    4,    9,    0,
         2,    59,   0,    2,    58,   7,    8,    62,   2,    5,    6,    61,
         64,   66,   0,    6,    9,    1,    4,    8,    2,    71,   72,   29,
         70,   74,   0,    4,    8,    2,    4,    7,    0,    3,    8,    79,
         80,   82,   0,    7,    8,    2,    7,    86,   4,    6,    87,   0,
         6,    8,    2,    4,    92,   88,   90,   95,   0,    2,    4,    1,
         6,    98,   2,    4,    99,   8,    100,  103,  101,  102,  104,  9,
         104,  106,  1,    4,    6,    0,    9,    110,  2,    8,    110,  29,
         112,  114,  0,    3,    6,    4,    52,   118,  80,   118,  121,  0,
         4,    6,    1,    8,    124,  0,    2,    9,    0,    4,    128,  6,
         9,    130,  4,    6,    131,  128,  133,  134,  0,    2,    5,    3,
         6,    78,   93,   138,  140,  0,    9,    28,   2,    4,    9,    0,
         6,    147,  145,  146,  148,  4,    8,    71,   2,    4,    8,    28,
         152,  155,  4,    6,    8,    0,    8,    159,  2,    5,    158,  2,
         6,    83,   160,  163,  164,  1,    2,    6,    0,    3,    4,    8,
         168,  170,  3,    6,    18,   1,    18,   174,  4,    9,    176,  5,
         8,    176,  177,  178,  180,  2,    82,   110,  2,    83,   110,  82,
         185,  186,  2,    7,    78,   99,   158,  190,  0,    5,    6,    0,
         3,    194,  6,    8,    197,  4,    8,    52,   4,    7,    8,    2,
         6,    200,  1,    202,  204,  0,    201,  206,  0,    6,    10,   6,
         9,    10,   0,    211,  212,  6,    9,    98,   1,    80,   216,  0,
         99,   218,  4,    6,    53,   3,    52,   222,  1,    52,   224,  3,
         6,    170,  2,    8,    228,  8,    128,  231,  2,    6,    8,    3,
         4,    8,    1,    234,  236,  1,    6,    146,  6,    146,  241,  0,
         9,    242,  0,    240,  245,  2,    5,    8,    4,    6,    248,  1,
         8,    250,  0,    9,    252,  251,  252,  254,  10,   131,  194,  4,
         7,    248,  0,    6,    249,  79,   260,  262,  0,    4,    7,    6,
         8,    266,  3,    6,    8,    18,   269,  270,  2,    7,    8,    4,
         82,   275,  5,    80,   276,  2,    8,    266,  4,    8,    281,  2,
         7,    282,  0,    281,  284,  5,    8,    28,   0,    4,    29,   110,
         288,  290,  0,    2,    110,  8,    110,  294,  1,    6,    236,  128,
         159,  298,  4,    6,    83,   2,    4,    303,  274,  302,  305,  6,
         58,   128,  8,    159,  308,  129,  308,  310,  5,    6,    170,  2,
         7,    170,  4,    8,    316,  1,    314,  318,  2,    6,    9,    0,
         249,  322,  0,    110,  325,  8,    324,  327,  2,    9,    170,  4,
         6,    171,  1,    6,    8,    330,  333,  334,  2,    5,    266,  6,
         8,    338,  2,    8,    267,  0,    341,  342,  3,    4,    6,    0,
         8,    110,  110,  347,  348,  4,    8,    170,  125,  168,  352,  0,
         9,    346,  1,    2,    8,    4,    194,  358,  356,  358,  361,  3,
         6,    266,  1,    2,    266,  0,    2,    6,    4,    8,    368,  364,
         366,  371,  7,    26,   128,  3,    6,    374,  27,   374,  376,  4,
         9,    66,   0,    67,   380,  5,    380,  382,  2,    145,  346,  8,
         66,   139,  7,    66,   346,  1,    8,    390,  6,    8,    80,   0,
         28,   395,  8,    395,  396,  1,    10,   12,   0,    3,    26,   2,
         9,    402,  0,    6,    26,   402,  404,  407,  4,    6,    129,  8,
         128,  410,  4,    7,    412,  5,    410,  414,  2,    8,    158,  8,
         28,   419,  4,    71,   128,  5,    410,  422,  1,    6,    10,   3,
         8,    10,   0,    5,    10,   426,  428,  430,  3,    4,    86,   2,
         26,   434,  87,   434,  436,  2,    7,    266,  8,    267,  440,  4,
         267,  442,  4,    6,    369,  8,    368,  446,  5,    446,  448,  2,
         4,    93,   3,    138,  452,  2,    8,    194,  3,    10,   456,  0,
         8,    154,  6,    155,  460,  0,    7,    154,  1,    462,  464,  4,
         9,    196,  4,    194,  469,  8,    468,  471,  1,    12,   98,   1,
         4,    334,  1,    6,    80,   2,    8,    479,  48,   80,   481,  2,
         29,   70,   10,   29,   484,  0,    4,    70,   52,   346,  489,  0,
         8,    93,   2,    93,   492,  4,    7,    92,   170,  494,  497,  3,
         6,    160,  146,  159,  500,  1,    2,    202,  29,   70,   504,  8,
         98,   334,  4,    6,    78,   4,    6,    9,    3,    78,   512,  154,
         511,  514,  0,    2,    67,   8,    171,  518,  6,    67,   520,  0,
         2,    27,   26,   235,  524,  6,    8,    524,  5,    26,   524,  4,
         529,  530,  3,    4,    194,  1,    456,  534,  1,    4,    270,  5,
         6,    538,  0,    8,    540,  271,  538,  542,  1,    2,    110,  112,
         358,  547,  4,    9,    82,   2,    6,    29,   29,   550,  552,  4,
         128,  202,  4,    202,  557,  128,  557,  558,  3,    10,   234,  0,
         5,    346,  4,    9,    346,  347,  564,  566,  4,    6,    358,  1,
         234,  570,  0,    6,    29,   43,   154,  574,  5,    86,   368,  4,
         371,  578,  6,    129,  190,  4,    9,    168,  0,    29,   584,  6,
         8,    98,   2,    118,  589,  4,    8,    98,   589,  590,  592,  130,
         159,  270,  1,    8,    28,   0,    4,    271,  8,    465,  600,  10,
         248,  346,  0,    2,    249,  6,    8,    249,  1,    2,    608,  29,
         606,  610,  6,    8,    195,  4,    194,  615,  5,    8,    128,  8,
         128,  158,  4,    618,  621,  0,    147,  240,  202,  240,  624,  2,
         8,    346,  1,    160,  356,  8,    81,   98,   8,    70,   633,  3,
         4,    26,   159,  524,  636,  26,   58,   589,  0,    28,   159,  159,
         236,  642,  5,    8,    18,   2,    8,    18,   146,  646,  649,  4,
         6,    139,  4,    8,    138,  5,    652,  654,  3,    8,    110,  2,
         111,  658,  0,    8,    513,  658,  660,  663,  2,    6,    73,   71,
         158,  666,  0,    6,    67,   3,    4,    66,   8,    671,  672,  66,
         158,  369,  6,    129,  154,  0,    4,    169,  8,    169,  680,  8,
         680,  683,  168,  682,  685,  4,    8,    19,   2,    99,   688,  1,
         8,    110,  0,    9,    692,  111,  692,  694,  7,    8,    128,  0,
         4,    129,  346,  698,  701,  9,    194,  202,  2,    5,    202,  3,
         704,  706,  2,    9,    124,  2,    346,  711,  4,    8,    70,   1,
         2,    714,  29,   70,   716,  6,    26,   407,  0,    407,  720,  0,
         4,    159,  7,    8,    724,  6,    159,  726,  6,    8,    159,  2,
         4,    730,  1,    158,  732,  158,  732,  735,  0,    734,  737,  2,
         4,    335,  2,    5,    334,  3,    740,  742,  1,    92,   744,  2,
         7,    72,   9,    402,  748,  0,    2,    29,   1,    158,  752,  0,
         29,   146,  4,    7,    358,  8,    10,   759,  4,    8,    66,   8,
         66,   763,  266,  763,  764,  5,    6,    274,  93,   170,  768,  2,
         129,  158,  0,    4,    235,  2,    9,    774,  235,  248,  776,  5,
         6,    78,   1,    4,    780,  7,    780,  782,  5,    6,    202,  9,
         202,  786,  0,    3,    158,  6,    202,  791,  2,    159,  790,  0,
         792,  795,  0,    9,    146,  2,    346,  799,  6,    8,    10,   4,
         8,    92,   4,    6,    805,  0,    3,    806,  274,  805,  808,  29,
         70,   154,  6,    8,    81,   1,    6,    814,  0,    7,    816,  815,
         816,  818,  4,    8,    269,  2,    266,  823,  1,    268,  824,  0,
         8,    81,   71,   146,  828,  0,    2,    71,   4,    6,    832,  70,
         154,  835,  5,    6,    128,  4,    8,    839,  4,    8,    838,  838,
         840,  843,  0,    4,    202,  2,    6,    203,  1,    4,    848,  5,
         846,  850,  0,    9,    18,   59,   110,  854,  0,    4,    275,  4,
         93,   274,  5,    858,  860,  1,    4,    66,   0,    7,    66,   129,
         864,  866,  6,    8,    791,  0,    4,    870,  2,    4,    159,  790,
         873,  874,  1,    78,   194,  2,    8,    99,   4,    7,    98,   1,
         86,   98,   880,  882,  885,  8,    111,  170,  6,    111,  170,  112,
         888,  891,  3,    8,    512,  0,    4,    894,  0,    7,    894,  512,
         897,  898,  2,    4,    147,  6,    8,    903,  7,    146,  904,  0,
         8,    903,  904,  906,  909,  2,    8,    98,   2,    268,  913,  1,
         8,    18,   4,    194,  916,  1,    194,  918,  2,    4,    155,  0,
         7,    922,  8,    465,  924,  2,    4,    334,  0,    95,   928,  3,
         6,    72,   0,    9,    932,  4,    6,    935,  128,  932,  937,  1,
         12,   740,  1,    2,    170,  5,    170,  942,  6,    8,    944,  7,
         942,  946,  945,  946,  948,  2,    93,   158,  0,    95,   952,  6,
         8,    93,   8,    92,   98,   0,    956,  959,  4,    8,    195,  2,
         9,    194,  11,   962,  964,  4,    270,  539,  92,   538,  969,  0,
         7,    146,  1,    92,   972,  1,    334,  928,  6,    8,    589,  3,
         4,    978,  0,    4,    978,  588,  980,  983,  1,    4,    274,  4,
         8,    159,  158,  986,  989,  2,    8,    155,  4,    6,    992,  1,
         154,  994,  4,    992,  997,  0,    155,  996,  6,    998,  1001, 0,
         99,   102,  6,    8,    1005, 2,    6,    266,  168,  268,  1009, 0,
         6,    155,  154,  589,  1012, 1,    8,    158,  3,    4,    1016, 128,
         159,  1018, 1,    6,    154,  2,    4,    1023, 8,    465,  1024, 4,
         7,    18,   6,    589,  1028, 6,    124,  237,  4,    6,    82,   236,
         1032, 1035, 8,    110,  368,  87,   236,  706,  3,    4,    70,   2,
         29,   1042, 2,    6,    138,  28,   248,  1047, 3,    6,    48,   71,
         146,  1050, 7,    8,    98,   0,    6,    99,   8,    99,   1056, 9,
         1054, 1058, 4,    52,   81,   1,    4,    234,  0,    1063, 1064, 0,
         3,    154,  66,   93,   1068, 99,   588,  740,  2,    8,    111,  49,
         1050, 1074, 3,    358,  570,  0,    9,    570,  571,  1078, 1080, 2,
         8,    124,  7,    124,  1084, 4,    8,    1086, 4,    1084, 1089, 8,
         1089, 1090, 159,  248,  346,  0,    235,  1094, 0,    358,  589,  6,
         589,  1098, 0,    8,    478,  2,    4,    81,   478,  1102, 1105, 4,
         8,    81,   0,    3,    80,   334,  1109, 1110, 4,    71,   138,  5,
         6,    1114, 235,  1114, 1116, 1,    6,    26,   2,    6,    26,   128,
         1120, 1123, 3,    4,    52,   6,    52,   1127, 5,    8,    52,   2,
         6,    53,   1129, 1130, 1132, 1,    4,    698,  128,  155,  1136, 87,
         236,  646,  3,    6,    52,   5,    6,    52,   248,  1142, 1145, 10,
         29,   70,   70,   147,  358,  7,    70,   1150, 2,    4,    86,   4,
         18,   1155, 8,    87,   1156, 0,    8,    237,  6,    52,   236,  6,
         236,  1161, 1160, 1163, 1164, 0,    3,    146,  6,    8,    1168, 6,
         1168, 1171, 146,  1170, 1173, 0,    29,   274,  9,    334,  1176, 7,
         8,    28,   0,    29,   1180, 1,    6,    1180, 9,    1182, 1184, 2,
         8,    170,  1,    314,  1188, 0,    8,    87,   6,    86,   1193, 2,
         6,    158,  0,    154,  1197, 1,    2,    158,  155,  1198, 1200, 19,
         234,  266,  4,    8,    235,  0,    6,    234,  3,    4,    1208, 6,
         1206, 1211, 1,    6,    922,  8,    154,  1215, 9,    1214, 1216, 155,
         1216, 1218, 2,    9,    368,  4,    7,    1222, 4,    9,    368,  6,
         1224, 1227, 3,    28,   288,  4,    86,   237,  2,    4,    1233, 86,
         1233, 1234}};
    inline static const std::vector<uint16_t> nodes10{
        {4,    222,  10,   17,   21,   25,   29,   33,   35,   17,   29,   21,
         37,   10,   46,   56,   66,   70,   74,   78,   82,   84,   88,   90,
         10,   100,  108,  112,  116,  118,  122,  126,  130,  140,  144,  10,
         153,  159,  163,  167,  171,  175,  177,  181,  185,  189,  10,   194,
         198,  198,  204,  206,  208,  212,  204,  214,  206,  2,    224,  230,
         10,   240,  250,  258,  264,  276,  280,  286,  294,  296,  300,  10,
         308,  316,  320,  326,  330,  334,  336,  340,  344,  350,  4,    352,
         360,  362,  364,  10,   374,  384,  390,  392,  398,  404,  414,  398,
         392,  422,  10,   431,  439,  443,  453,  463,  473,  481,  489,  499,
         443,  2,    506,  510,  10,   514,  518,  526,  530,  536,  538,  542,
         546,  550,  552,  4,    557,  559,  561,  563,  9,    571,  579,  587,
         593,  599,  607,  613,  617,  623,  2,    626,  632,  10,   639,  643,
         639,  643,  649,  651,  653,  655,  655,  649,  10,   663,  673,  679,
         685,  689,  693,  697,  701,  705,  709,  10,   718,  728,  738,  744,
         754,  758,  764,  768,  776,  780,  2,    783,  785,  10,   792,  800,
         804,  812,  804,  816,  824,  824,  832,  840,  10,   846,  852,  856,
         860,  864,  868,  872,  876,  878,  882,  10,   889,  893,  899,  903,
         909,  913,  917,  923,  929,  935,  10,   937,  941,  943,  945,  949,
         953,  955,  957,  961,  965,  10,   970,  980,  988,  996,  1000, 1006,
         1014, 1024, 1032, 1038, 10,   1044, 1046, 1050, 1052, 1056, 1060, 1062,
         1064, 1068, 1062, 10,   1070, 1074, 1080, 1070, 1082, 1084, 1088, 1096,
         1102, 1108, 10,   1111, 1115, 1119, 1123, 1129, 1131, 1135, 1141, 1145,
         1149, 10,   1156, 1164, 1168, 1170, 1174, 1178, 1180, 1182, 1184, 1186,
         2,    1191, 1193, 10,   1197, 1203, 1205, 1209, 1211, 1203, 1215, 1217,
         1221, 1223, 10,   1228, 1236, 1240, 1244, 1252, 1256, 1264, 1268, 1274,
         1278, 10,   1283, 1287, 1293, 1297, 1305, 1311, 1319, 1323, 1325, 1327,
         8,    1332, 1338, 1344, 1350, 1358, 1364, 1368, 1374, 10,   1378, 1380,
         1384, 1388, 1394, 1396, 1402, 1406, 1410, 1412, 10,   1418, 1422, 1428,
         1432, 1436, 1440, 1442, 1444, 1448, 1452, 2,    1458, 1462, 10,   1469,
         1473, 1477, 1483, 1487, 1489, 1493, 1487, 1497, 1501, 7,    875,  1503,
         1507, 1509, 845,  1511, 1513, 8,    1516, 1524, 1530, 1538, 1542, 1550,
         1558, 1566, 10,   1573, 1577, 1581, 1589, 1593, 1597, 1601, 1607, 1611,
         1615, 10,   1620, 1630, 1636, 1642, 1648, 1654, 1658, 1664, 1668, 1674,
         10,   1681, 1685, 1691, 1697, 1701, 1707, 1711, 1713, 1717, 1719, 10,
         1724, 1728, 1732, 1734, 1738, 1744, 1750, 1752, 1760, 1764, 2,    1768,
         1772, 10,   1778, 1782, 1786, 1790, 1798, 1806, 1810, 1812, 1816, 1822,
         6,    1825, 1829, 1833, 1837, 1841, 1843, 10,   1845, 1849, 1853, 1859,
         1863, 1865, 1869, 1875, 1879, 1885, 10,   1888, 1892, 1898, 1904, 1908,
         1912, 1920, 1926, 1934, 1938, 10,   1944, 1948, 1956, 1962, 1962, 1972,
         1976, 1986, 1990, 1994, 10,   2002, 2006, 2010, 2016, 2020, 2024, 2016,
         2028, 2032, 2036, 10,   2042, 2044, 2046, 2048, 2050, 2052, 2054, 2056,
         2058, 2060, 9,    2063, 2063, 2067, 2069, 2071, 2073, 2069, 2077, 2071,
         2,    2079, 2081, 10,   2085, 809,  809,  2089, 2085, 789,  2093, 797,
         797,  2097, 10,   2100, 2104, 2108, 2114, 2120, 2124, 2130, 2134, 2136,
         2140, 10,   2143, 2145, 2147, 2151, 2153, 2155, 2159, 2161, 2165, 2167,
         10,   2172, 2176, 2172, 2182, 2186, 2190, 2190, 2194, 2186, 2200, 10,
         2207, 2211, 2217, 2225, 2227, 2231, 2233, 2237, 2239, 2241, 10,   2245,
         2249, 2251, 2253, 2255, 2259, 2263, 2267, 2269, 2271, 10,   2277, 2281,
         2283, 2285, 2287, 2289, 2293, 2297, 2301, 2303, 10,   2309, 2315, 2321,
         2329, 2331, 2335, 2331, 2337, 2343, 2345, 1,    0,    10,   2351, 2355,
         2359, 2363, 2371, 2375, 2379, 2381, 2383, 2387, 10,   2391, 2395, 2399,
         2403, 2407, 2411, 2413, 2417, 2419, 2425, 10,   2431, 2435, 2441, 2445,
         2447, 2447, 2445, 2453, 2459, 2465, 10,   2468, 2474, 2478, 2482, 2484,
         2486, 2490, 2492, 2494, 2498, 7,    2503, 2505, 2507, 2511, 2513, 2515,
         2521, 10,   2527, 2533, 2535, 2541, 2543, 2545, 2549, 2551, 2555, 2557,
         10,   2560, 2564, 2566, 2568, 2570, 2578, 2584, 2590, 2594, 2596, 10,
         2601, 2603, 2607, 2609, 2611, 2603, 2615, 2617, 2619, 2617, 4,    2621,
         2623, 1535, 1547, 5,    2626, 2632, 2636, 2640, 2632, 10,   2644, 2650,
         2656, 2660, 2662, 2666, 2670, 2672, 2674, 2678, 10,   2683, 2687, 2693,
         2697, 2701, 2707, 2711, 2717, 2721, 2729, 10,   2732, 2738, 2746, 2752,
         2758, 2764, 2772, 2780, 2786, 2790, 10,   2794, 2800, 2806, 2808, 2810,
         2814, 2816, 2822, 2828, 2830, 8,    2832, 2834, 2832, 2834, 2834, 2832,
         2832, 2834, 10,   2837, 2841, 2845, 2847, 2849, 2851, 2855, 2857, 2859,
         2861, 10,   2867, 2877, 2885, 2889, 2893, 2897, 2905, 2911, 2915, 2919,
         10,   2923, 2931, 2937, 2941, 2947, 2953, 2959, 2963, 2969, 2971, 10,
         2972, 2978, 2980, 2982, 2972, 2986, 2988, 2994, 2998, 2982, 10,   3006,
         3014, 3018, 3022, 3026, 3030, 3034, 3038, 3042, 3046, 5,    3049, 3051,
         3053, 3057, 3059, 1,    9,    10,   3065, 3069, 3077, 3069, 3081, 3087,
         3095, 3099, 3081, 3103, 10,   3104, 3112, 3114, 3120, 3122, 3128, 3136,
         3138, 3142, 3144, 1,    657,  10,   3146, 3154, 3160, 3164, 3172, 3180,
         3186, 3190, 3192, 3194, 10,   3196, 3200, 3202, 3204, 3206, 3214, 3218,
         3220, 3222, 3228, 6,    3233, 3235, 3237, 3239, 3241, 3243, 10,   3246,
         3248, 3250, 3252, 3254, 3256, 3260, 3262, 3268, 3270, 10,   3273, 3277,
         487,  3281, 3283, 3285, 3287, 3291, 3293, 441,  2,    3294, 3294, 10,
         3296, 3302, 3306, 3310, 3314, 3296, 3318, 3324, 3330, 3332, 10,   3335,
         3339, 3341, 3345, 3349, 3351, 3355, 3359, 3361, 3365, 10,   3366, 3368,
         3370, 3372, 3376, 3378, 3366, 3378, 3380, 3370, 10,   3386, 3392, 3396,
         3400, 3410, 3414, 3418, 3426, 3432, 3436, 10,   3440, 3442, 3446, 3452,
         3454, 3458, 3462, 3464, 3468, 3474, 1,    191,  6,    3477, 3479, 3477,
         3485, 3477, 3491, 10,   3493, 3495, 3497, 3499, 3503, 3507, 3511, 3513,
         3515, 3519, 10,   3524, 3530, 3534, 3540, 3548, 3556, 3562, 3570, 3574,
         3582, 10,   3584, 3586, 3588, 3590, 3584, 3592, 3594, 3596, 3598, 3600,
         10,   3604, 3608, 3612, 3616, 3618, 3622, 3628, 3634, 3640, 3646, 10,
         3653, 3653, 3657, 3663, 3665, 3667, 3669, 3671, 3673, 3679, 4,    1997,
         1425, 2133, 2041, 10,   3680, 3682, 3684, 3688, 3690, 3694, 3696, 3700,
         3702, 3704, 10,   3706, 3712, 3716, 3720, 3724, 3728, 3706, 3734, 3736,
         3740, 10,   3744, 3748, 3752, 3756, 3760, 3764, 3766, 3772, 3776, 3782,
         10,   3788, 3792, 3796, 3800, 3802, 3806, 3792, 3808, 3814, 3800, 10,
         3820, 3824, 3830, 3834, 3836, 3838, 3844, 3848, 3852, 3860, 10,   3868,
         3872, 3880, 3884, 3892, 3900, 3908, 3916, 3922, 3926, 10,   3929, 3933,
         3939, 3941, 3943, 3947, 3949, 3951, 3953, 3957, 10,   3963, 3973, 3981,
         3989, 3995, 4001, 4009, 4013, 4019, 4025, 10,   4027, 4033, 4027, 4039,
         4047, 4051, 4055, 4061, 4065, 4067, 10,   4071, 4075, 4077, 4081, 4083,
         4087, 4091, 4087, 4077, 4097, 3,    4099, 4101, 4103, 2,    4105, 4107,
         10,   4108, 4110, 4112, 4116, 4120, 4124, 4130, 4136, 4142, 4148, 10,
         4153, 4157, 4161, 4165, 4169, 4173, 4177, 4179, 4181, 4187, 10,   4188,
         4192, 4194, 4196, 4198, 4200, 4204, 4206, 4198, 4200, 1,    4210, 10,
         4214, 4216, 4222, 4226, 4230, 4234, 4238, 4242, 4246, 4252, 6,    4257,
         4259, 4261, 4265, 4267, 4269, 10,   4270, 4276, 4280, 4284, 4288, 4294,
         4294, 4270, 4288, 4300, 10,   4302, 4304, 4306, 4308, 4310, 4316, 4320,
         4324, 4326, 4330, 10,   4332, 4336, 4340, 4346, 4350, 4356, 4360, 4364,
         4368, 4374, 10,   4382, 4388, 4394, 4400, 4404, 4408, 4414, 4416, 4418,
         4422, 10,   4433, 4437, 4447, 4453, 4457, 4459, 4465, 4467, 4471, 4475,
         5,    4480, 4486, 4490, 4496, 4498, 10,   4501, 4505, 4507, 4509, 4511,
         4513, 4517, 4519, 4525, 4529, 2,    4530, 4532, 10,   4537, 4539, 4541,
         4543, 4545, 4549, 4551, 4555, 4559, 4563, 10,   4568, 4574, 4578, 4582,
         4588, 4594, 4602, 4608, 4588, 4594, 10,   4610, 4612, 4614, 4616, 4618,
         4622, 4624, 4626, 4628, 4630, 10,   4635, 4637, 4639, 4641, 4643, 4645,
         4649, 4651, 4653, 4655, 10,   4660, 4664, 4666, 4672, 4678, 4682, 4688,
         4692, 4696, 4700, 10,   4705, 4707, 4709, 4711, 4715, 4719, 4723, 4727,
         4729, 4731, 10,   4735, 4737, 4739, 4741, 4743, 4743, 4739, 4737, 4745,
         4745, 1,    927,  10,   4751, 4755, 4757, 4763, 4765, 4769, 4773, 4775,
         4773, 4775, 10,   4777, 4781, 4785, 4787, 4789, 4793, 4795, 4797, 4799,
         4803, 1,    19,   10,   4808, 4812, 4816, 4824, 4830, 4834, 4838, 4842,
         4850, 4858, 4,    4860, 4862, 4864, 4866, 10,   4870, 4876, 4880, 4886,
         4888, 4894, 4896, 4902, 4908, 4914, 10,   4921, 4927, 4931, 4935, 4937,
         4927, 4943, 4949, 4953, 4959, 7,    4963, 4967, 4971, 4973, 4967, 4975,
         4979, 2,    4982, 4984, 10,   4990, 4994, 4996, 5002, 5004, 5010, 5014,
         5018, 5024, 5028, 10,   5031, 5039, 5043, 5051, 5055, 5059, 5061, 5063,
         5067, 5071, 10,   5077, 5081, 5085, 5089, 5085, 5089, 5093, 5097, 5101,
         5105, 10,   5110, 5114, 5118, 5110, 5122, 5128, 5132, 5136, 5138, 5144,
         10,   5149, 5155, 5157, 5161, 5163, 5167, 5171, 5173, 5177, 5181, 10,
         5186, 5192, 5198, 5186, 5204, 5208, 5212, 5218, 5224, 5204, 10,   5227,
         5229, 5231, 5233, 5235, 5237, 5239, 5241, 5243, 5239, 10,   5249, 5255,
         5259, 5267, 5271, 5277, 5283, 5287, 5297, 5305, 10,   5312, 5314, 5318,
         5322, 5330, 5336, 5340, 5344, 5348, 5352, 3,    5358, 5362, 5366, 10,
         5373, 5381, 5387, 5391, 5393, 5397, 5397, 5407, 5417, 5421, 10,   5423,
         5427, 5429, 5435, 5441, 5445, 5449, 5455, 5457, 5461, 10,   5463, 5467,
         5473, 5479, 5485, 5489, 5493, 5497, 5505, 5509, 10,   5515, 5517, 5521,
         5521, 5527, 5531, 5535, 5539, 5545, 5549, 10,   5550, 5556, 5560, 5564,
         5564, 5560, 5566, 5570, 5572, 5576, 10,   5580, 5590, 5594, 5600, 5604,
         5608, 5612, 5620, 5626, 5630, 5,    5635, 5639, 5635, 5639, 5641, 10,
         5647, 5653, 5657, 5661, 5663, 5669, 5675, 5681, 5689, 5695, 8,    5696,
         5698, 5696, 5702, 5706, 5698, 5710, 5714, 10,   5718, 5722, 5724, 5728,
         5734, 5740, 5746, 5752, 5758, 5764, 10,   5770, 5774, 5778, 5784, 5788,
         5790, 5794, 5798, 5800, 5806, 10,   5809, 5811, 5811, 5809, 5815, 5819,
         5823, 5825, 5829, 5815, 10,   5833, 5835, 5835, 5839, 5841, 1207, 5843,
         5845, 5847, 5845, 10,   5849, 5851, 5853, 5855, 5857, 5859, 5863, 5865,
         5867, 5869, 10,   5875, 5883, 5887, 5893, 5897, 5901, 5907, 5913, 5915,
         5917, 10,   5919, 5923, 5929, 5935, 5941, 5947, 5955, 5961, 5967, 5973,
         10,   5979, 5985, 5991, 5997, 6003, 6009, 6015, 6021, 6025, 6025, 10,
         6029, 6033, 6033, 6037, 6037, 5977, 829,  829,  6029, 821,  10,   6039,
         6045, 6047, 6051, 6057, 6063, 6065, 6069, 6071, 6073, 9,    6078, 6084,
         6086, 6088, 6092, 6094, 6096, 6098, 6102, 10,   6106, 6110, 6112, 6118,
         6122, 6126, 6134, 6138, 6142, 6144, 7,    6151, 6155, 6157, 6157, 6161,
         6163, 6155, 10,   6166, 6170, 6172, 6178, 6180, 6184, 6186, 6192, 6194,
         6196, 10,   6207, 6211, 6217, 6221, 6231, 6237, 6241, 6249, 6253, 6259,
         2,    1387, 4837, 10,   6265, 6269, 6273, 6277, 6283, 6285, 6287, 6291,
         6293, 6295, 10,   6296, 6298, 6300, 6304, 6306, 6308, 6310, 6296, 6312,
         6314, 10,   6319, 6323, 6327, 6331, 6335, 6339, 6341, 6343, 6349, 6353,
         2,    6357, 6361, 10,   6362, 6366, 6370, 6376, 6380, 6386, 6390, 6394,
         6398, 6402, 10,   6408, 6414, 6420, 6426, 6432, 6438, 6442, 6450, 6456,
         6460, 10,   6462, 6464, 6462, 6468, 6472, 6474, 6462, 6478, 6462, 6482,
         10,   6489, 6493, 6495, 6497, 6499, 6503, 6505, 6507, 6499, 6509, 10,
         6515, 6517, 6521, 6523, 6525, 6529, 6531, 6537, 6539, 6545, 1,    6550,
         10,   6555, 6559, 6563, 6567, 6573, 6577, 6581, 6583, 6585, 6589, 10,
         6592, 6594, 6602, 6608, 6614, 6618, 6620, 6626, 6632, 6636, 10,   6640,
         6646, 6652, 6658, 6662, 6664, 6668, 6672, 6676, 6680, 10,   6683, 6689,
         6691, 6697, 6703, 6709, 6715, 6721, 6723, 6725, 2,    6728, 6728, 10,
         6731, 6737, 6741, 6749, 6755, 6759, 6763, 6769, 6775, 6781, 10,   6784,
         6788, 6794, 6798, 6784, 6802, 6804, 6810, 6812, 6816, 10,   6823, 6831,
         6837, 6845, 6851, 6857, 6865, 6869, 6879, 6885, 10,   6886, 6892, 6898,
         6902, 6906, 6910, 6912, 6914, 6916, 6920, 6,    6925, 6929, 6933, 6935,
         6937, 6941, 4,    6945, 6947, 6949, 6953, 4,    6954, 6956, 6958, 6960,
         10,   6964, 6968, 6970, 6974, 6980, 6984, 6988, 6990, 6994, 6998, 10,
         7003, 7009, 7011, 7015, 7023, 7027, 7029, 7031, 7035, 7039, 10,   7046,
         7054, 7060, 7064, 7068, 7072, 7076, 7082, 7088, 7096, 10,   7103, 7107,
         7115, 7119, 7123, 7127, 7131, 7133, 7135, 7139, 10,   7142, 7144, 7148,
         7154, 7158, 7162, 7166, 7172, 7176, 7180, 10,   7186, 7190, 7196, 7200,
         7206, 7208, 7214, 7218, 7222, 7226, 10,   7229, 7231, 7233, 7235, 7237,
         7239, 7241, 7243, 7245, 7247, 10,   7248, 7250, 7252, 7254, 7250, 7254,
         7252, 5760, 5760, 7256, 10,   7262, 7268, 7272, 7276, 7280, 7284, 7286,
         7288, 7290, 7292, 5,    7295, 7297, 7299, 7301, 7303, 9,    7305, 7307,
         7311, 7317, 7319, 7323, 7329, 7333, 7339, 10,   7343, 7349, 7349, 7355,
         7359, 7363, 7367, 7371, 7349, 7375, 7,    7381, 7383, 7387, 7391, 7393,
         7399, 7403, 10,   7405, 7407, 7405, 7411, 7413, 7415, 7417, 7419, 7413,
         7421, 10,   7425, 7431, 7437, 7441, 7443, 7447, 7453, 7459, 7463, 7467,
         1,    2,    4,    7,    8,    10,   6,    8,    11,   9,    12,   14,
         6,    8,    10,   6,    12,   19,   8,    10,   13,   6,    12,   23,
         6,    9,    10,   7,    14,   26,   7,    8,    26,   11,   26,   30,
         11,   12,   26,   10,   14,   19,   0,    4,    7,    2,    4,    6,
         9,    38,   40,   8,    38,   40,   8,    42,   45,   0,    3,    4,
         0,    2,    6,    9,    48,   50,   8,    48,   50,   8,    52,   55,
         0,    5,    6,    3,    4,    6,    9,    58,   60,   8,    58,   60,
         8,    62,   65,   48,   50,   53,   8,    52,   69,   58,   60,   63,
         8,    62,   73,   8,    49,   50,   48,   55,   76,   8,    59,   60,
         58,   65,   80,   51,   52,   76,   9,    48,   76,   51,   76,   86,
         61,   62,   80,   2,    4,    8,    3,    6,    8,    0,    93,   94,
         0,    92,   94,   92,   96,   99,   5,    6,    8,    0,    40,   103,
         0,    41,   102,  1,    104,  106,  0,    92,   95,   1,    96,   110,
         1,    40,   102,  41,   104,  114,  103,  106,  114,  1,    40,   106,
         103,  106,  120,  1,    92,   94,   95,   96,   124,  1,    92,   96,
         95,   96,   128,  2,    5,    8,    2,    6,    9,    0,    132,  135,
         0,    133,  134,  1,    136,  138,  1,    132,  134,  135,  138,  142,
         2,    5,    6,    3,    8,    146,  2,    8,    146,  2,    148,  151,
         7,    8,    40,   6,    8,    40,   6,    154,  157,  6,    8,    41,
         9,    154,  160,  6,    9,    40,   41,   154,  164,  6,    9,    154,
         41,   154,  168,  2,    9,    146,  147,  148,  172,  7,    160,  164,
         2,    8,    147,  3,    172,  178,  8,    146,  149,  2,    148,  183,
         8,    40,   155,  6,    154,  187,  1,    8,    40,   8,    40,   191,
         0,    190,  193,  0,    8,    40,   0,    190,  197,  0,    8,    41,
         0,    9,    40,   1,    200,  202,  9,    190,  200,  41,   190,  202,
         0,    9,    190,  41,   190,  210,  40,   197,  200,  0,    2,    8,
         0,    5,    8,    2,    6,    218,  4,    7,    218,  217,  220,  222,
         3,    6,    216,  4,    6,    217,  218,  227,  228,  0,    7,    8,
         2,    4,    232,  5,    6,    232,  2,    216,  236,  234,  236,  239,
         1,    2,    8,    5,    8,    242,  0,    6,    245,  8,    41,   246,
         242,  245,  248,  0,    9,    92,   7,    8,    252,  6,    41,   254,
         1,    252,  256,  2,    4,    255,  6,    254,  261,  1,    252,  262,
         0,    2,    4,    0,    9,    266,  7,    8,    268,  2,    4,    271,
         6,    270,  273,  1,    268,  274,  6,    41,   270,  1,    268,  278,
         0,    6,    9,    8,    41,   282,  1,    252,  284,  0,    9,    234,
         2,    4,    233,  6,    232,  291,  1,    288,  292,  1,    252,  292,
         6,    41,   232,  1,    252,  298,  0,    4,    9,    7,    242,  302,
         2,    4,    305,  6,    304,  307,  1,    4,    8,    0,    2,    9,
         6,    311,  312,  41,   310,  314,  7,    310,  312,  5,    60,   318,
         1,    8,    60,   5,    312,  322,  7,    60,   324,  7,    312,  322,
         5,    60,   328,  6,    243,  302,  41,   242,  332,  41,   312,  322,
         4,    6,    61,   312,  322,  339,  2,    4,    319,  6,    318,  343,
         4,    6,    313,  1,    8,    346,  41,   312,  348,  41,   310,  312,
         0,    3,    8,    0,    4,    8,    2,    4,    7,    354,  357,  358,
         217,  218,  358,  41,   242,  302,  2,    6,    49,   3,    8,    48,
         0,    4,    369,  6,    8,    370,  366,  368,  373,  0,    2,    5,
         4,    6,    377,  5,    8,    376,  6,    8,    266,  378,  380,  383,
         0,    2,    378,  6,    8,    386,  378,  380,  389,  366,  368,  383,
         0,    6,    11,   1,    8,    10,   383,  394,  396,  0,    4,    366,
         6,    8,    400,  366,  368,  403,  0,    6,    359,  7,    8,    358,
         2,    4,    409,  0,    8,    410,  406,  408,  413,  2,    7,    48,
         1,    48,   102,  2,    8,    48,   416,  418,  421,  1,    6,    266,
         9,    10,   424,  10,   424,  427,  8,    426,  429,  1,    2,    60,
         8,    338,  432,  9,    338,  432,  8,    435,  436,  8,    10,   424,
         8,    426,  441,  2,    4,    11,   1,    6,    444,  9,    10,   446,
         8,    10,   446,  8,    448,  451,  0,    5,    10,   2,    6,    455,
         9,    10,   456,  8,    10,   456,  8,    458,  461,  0,    3,    10,
         4,    6,    465,  9,    10,   466,  8,    10,   466,  8,    468,  471,
         4,    6,    49,   9,    10,   474,  8,    10,   474,  8,    476,  479,
         2,    6,    377,  9,    10,   482,  8,    10,   482,  8,    484,  487,
         1,    2,    6,    4,    6,    490,  9,    10,   492,  8,    10,   492,
         8,    494,  497,  1,    4,    6,    0,    9,    500,  2,    8,    500,
         41,   502,  504,  3,    8,    40,   200,  500,  509,  4,    312,  491,
         41,   490,  512,  5,    312,  490,  4,    41,   516,  1,    6,    358,
         0,    9,    358,  3,    520,  522,  5,    358,  524,  5,    520,  522,
         3,    358,  528,  2,    9,    376,  4,    6,    376,  60,   532,  535,
         41,   520,  522,  4,    8,    48,   60,   416,  541,  3,    6,    48,
         358,  541,  544,  2,    6,    517,  4,    516,  549,  41,   378,  532,
         0,    4,    6,    1,    8,    554,  4,    8,    39,   6,    8,    59,
         6,    8,    310,  4,    7,    266,  2,    9,    564,  6,    8,    564,
         267,  566,  568,  1,    2,    38,   2,    8,    38,   6,    8,    38,
         572,  575,  576,  2,    9,    266,  4,    6,    267,  6,    9,    266,
         580,  582,  585,  2,    8,    267,  7,    8,    266,  564,  588,  591,
         4,    7,    580,  6,    8,    580,  267,  594,  596,  1,    4,    312,
         5,    6,    312,  6,    9,    312,  600,  602,  605,  3,    8,    38,
         7,    8,    38,   572,  608,  611,  6,    8,    267,  582,  588,  615,
         4,    6,    312,  6,    8,    312,  600,  619,  620,  2,    7,    356,
         267,  282,  624,  0,    6,    8,    3,    6,    356,  376,  629,  630,
         2,    4,    9,    0,    6,    635,  203,  634,  636,  0,    7,    634,
         6,    203,  640,  1,    6,    634,  0,    8,    644,  41,   644,  646,
         8,    191,  644,  0,    203,  644,  41,   196,  644,  1,    6,    8,
         0,    4,    656,  3,    4,    8,    40,   659,  660,  2,    6,    8,
         4,    9,    664,  1,    6,    666,  4,    664,  669,  8,    666,  671,
         0,    6,    358,  4,    8,    675,  359,  634,  676,  0,    8,    147,
         4,    6,    681,  132,  147,  682,  4,    8,    283,  359,  634,  686,
         4,    8,    555,  359,  634,  690,  6,    9,    310,  132,  147,  694,
         6,    9,    500,  132,  147,  698,  7,    8,    500,  359,  634,  702,
         7,    8,    310,  359,  634,  706,  6,    8,    313,  4,    7,    710,
         0,    5,    712,  312,  712,  714,  9,    710,  716,  0,    3,    134,
         5,    8,    720,  1,    4,    722,  134,  722,  724,  7,    720,  726,
         6,    8,    39,   0,    3,    730,  6,    9,    38,   2,    730,  734,
         7,    732,  736,  2,    9,    614,  7,    218,  266,  3,    740,  742,
         0,    3,    6,    1,    8,    746,  5,    6,    748,  9,    266,  746,
         7,    750,  752,  4,    7,    748,  5,    752,  756,  0,    5,    590,
         9,    590,  746,  1,    760,  762,  1,    4,    590,  5,    762,  766,
         6,    8,    565,  0,    3,    770,  9,    266,  772,  7,    770,  774,
         9,    574,  732,  7,    730,  778,  8,    48,   490,  8,    10,   746,
         6,    41,   358,  1,    8,    786,  0,    8,    786,  0,    788,  791,
         3,    146,  358,  1,    8,    794,  0,    8,    794,  0,    796,  799,
         8,    786,  789,  0,    788,  803,  4,    41,   146,  1,    8,    806,
         8,    806,  809,  0,    808,  811,  0,    8,    806,  0,    808,  815,
         1,    48,   376,  6,    8,    819,  6,    8,    818,  818,  820,  823,
         5,    10,   48,   6,    8,    827,  6,    8,    826,  826,  828,  831,
         5,    10,   464,  6,    8,    835,  6,    8,    834,  834,  836,  839,
         2,    355,  500,  2,    354,  500,  354,  842,  845,  8,    313,  500,
         9,    312,  848,  501,  848,  850,  3,    354,  842,  501,  842,  854,
         3,    354,  500,  501,  842,  858,  9,    312,  500,  501,  848,  862,
         2,    354,  501,  3,    842,  866,  8,    312,  501,  9,    848,  870,
         8,    312,  500,  312,  848,  875,  2,    845,  858,  354,  500,  859,
         2,    858,  881,  4,    7,    10,   5,    10,   746,  8,    884,  886,
         7,    8,    132,  48,   490,  890,  5,    6,    490,  7,    8,    894,
         48,   490,  896,  2,    8,    41,   48,   490,  900,  4,    6,    9,
         2,    8,    905,  48,   490,  906,  5,    8,    358,  48,   490,  910,
         7,    8,    146,  48,   490,  914,  4,    7,    490,  5,    8,    918,
         48,   490,  920,  2,    8,    376,  4,    6,    8,    51,   924,  926,
         6,    8,    48,   1,    2,    930,  905,  930,  932,  8,    10,   656,
         2,    6,    48,   1,    8,    938,  4,    132,  656,  2,    656,  660,
         0,    6,    10,   1,    8,    946,  4,    6,    50,   1,    8,    950,
         8,    634,  641,  1,    8,    534,  0,    6,    634,  1,    8,    958,
         1,    2,    660,  6,    8,    962,  0,    2,    474,  8,    48,   475,
         421,  966,  968,  2,    7,    8,    0,    3,    972,  4,    7,    974,
         2,    973,  976,  357,  974,  978,  9,    38,   664,  0,    8,    983,
         38,   665,  984,  39,   982,  986,  9,    38,   50,   3,    8,    990,
         6,    39,   992,  7,    990,  994,  39,   50,   992,  7,    990,  998,
         7,    8,    990,  2,    39,   1002, 3,    990,  1004, 8,    747,  904,
         2,    4,    1008, 0,    8,    1011, 9,    1008, 1012, 4,    6,    747,
         8,    747,  1016, 2,    4,    1018, 0,    8,    1021, 9,    1018, 1022,
         6,    9,    48,   0,    2,    1026, 4,    7,    8,    421,  1028, 1030,
         217,  218,  904,  0,    2,    1034, 7,    1034, 1036, 0,    3,    146,
         4,    9,    146,  7,    1040, 1042, 7,    26,   394,  6,    9,    634,
         7,    636,  1048, 9,    12,   394,  7,    8,    634,  9,    636,  1054,
         0,    7,    10,   9,    394,  1058, 9,    636,  640,  9,    14,   1058,
         6,    8,    635,  9,    640,  1066, 60,   376,  383,  0,    5,    490,
         48,   629,  1072, 9,    358,  656,  2,    4,    1077, 0,    1076, 1079,
         376,  544,  629,  282,  445,  1058, 2,    60,   267,  0,    383,  1086,
         0,    8,    359,  6,    358,  1091, 2,    4,    1093, 0,    1092, 1095,
         9,    358,  520,  2,    4,    1099, 0,    1098, 1101, 6,    358,  629,
         2,    4,    1105, 0,    1104, 1107, 216,  313,  500,  0,    2,    60,
         60,   216,  1113, 0,    2,    500,  216,  500,  1117, 0,    3,    432,
         8,    432,  1120, 0,    3,    500,  1,    2,    1124, 8,    1124, 1126,
         3,    216,  520,  3,    6,    38,   1,    216,  1132, 4,    7,    216,
         3,    6,    1136, 1,    216,  1138, 1,    6,    1136, 3,    216,  1142,
         1,    4,    146,  3,    216,  1146, 3,    8,    60,   0,    61,   1150,
         1,    2,    1152, 9,    1152, 1154, 0,    3,    132,  0,    7,    132,
         1,    2,    1160, 9,    1158, 1162, 3,    4,    58,   312,  354,  1167,
         312,  354,  631,  1,    6,    92,   242,  312,  1173, 0,    9,    242,
         242,  1173, 1176, 242,  312,  433,  242,  312,  1147, 242,  1147, 1176,
         312,  354,  1125, 0,    2,    7,    8,    10,   1189, 1,    660,  664,
         0,    283,  634,  1,    636,  1194, 7,    628,  634,  6,    628,  635,
         1,    1198, 1200, 635,  644,  1198, 7,    628,  644,  635,  644,  1206,
         1,    636,  1198, 1,    6,    1198, 635,  1198, 1212, 1,    640,  1200,
         8,    634,  657,  1,    636,  1218, 635,  644,  1218, 0,    6,    148,
         0,    7,    148,  6,    1225, 1226, 2,    6,    660,  1,    8,    1230,
         0,    9,    1232, 1231, 1232, 1234, 0,    9,    1230, 1231, 1232, 1238,
         1,    6,    148,  0,    1225, 1242, 5,    8,    60,   0,    6,    1246,
         1,    6,    1246, 0,    1249, 1250, 1,    8,    634,  282,  645,  1254,
         2,    4,    282,  1,    6,    1258, 1,    8,    1258, 282,  1261, 1262,
         0,    7,    40,   202,  232,  1267, 0,    7,    290,  0,    9,    290,
         232,  1271, 1272, 0,    8,    1230, 0,    1232, 1277, 2,    5,    356,
         60,   1113, 1280, 5,    356,  490,  1,    48,   1284, 4,    9,    48,
         0,    2,    1288, 48,   366,  1291, 2,    6,    1289, 48,   1291, 1294,
         4,    9,    746,  0,    2,    1298, 2,    4,    747,  746,  1301, 1302,
         5,    8,    10,   0,    2,    1307, 10,   394,  1309, 5,    8,    490,
         0,    2,    1313, 0,    4,    491,  490,  1315, 1316, 5,    216,  490,
         1,    48,   1320, 3,    10,   1320, 3,    10,   1284, 1,    6,    132,
         4,    6,    132,  302,  1328, 1331, 0,    6,    243,  4,    7,    242,
         357,  1334, 1336, 0,    7,    242,  4,    6,    243,  357,  1340, 1342,
         0,    6,    242,  5,    6,    242,  302,  1347, 1348, 2,    8,    303,
         1,    6,    1352, 4,    6,    1352, 302,  1354, 1357, 0,    6,    1352,
         5,    6,    1352, 302,  1361, 1362, 4,    6,    133,  357,  1160, 1366,
         0,    6,    133,  4,    7,    132,  357,  1370, 1372, 5,    134,  310,
         7,    720,  1376, 357,  1334, 1340, 0,    7,    102,  51,   134,  1382,
         6,    242,  356,  242,  1334, 1387, 6,    242,  357,  0,    7,    1390,
         243,  1390, 1392, 0,    1387, 1390, 7,    8,    312,  6,    218,  313,
         9,    1398, 1400, 1,    102,  134,  7,    720,  1404, 1,    134,  722,
         7,    720,  1408, 7,    1334, 1390, 5,    312,  664,  3,    4,    1414,
         7,    1414, 1416, 3,    522,  926,  5,    358,  1420, 6,    8,    358,
         3,    522,  1424, 5,    358,  1426, 5,    522,  1424, 3,    358,  1430,
         5,    312,  1424, 3,    358,  1434, 5,    522,  664,  3,    358,  1438,
         3,    358,  1414, 7,    60,   1414, 2,    155,  200,  4,    41,   1446,
         4,    155,  200,  2,    41,   1450, 3,    6,    1336, 4,    8,    1455,
         0,    1336, 1457, 4,    8,    1188, 0,    1336, 1461, 2,    9,    1370,
         0,    4,    1465, 6,    1371, 1466, 1,    132,  608,  6,    38,   1470,
         8,    267,  572,  6,    38,   1474, 2,    8,    58,   0,    134,  1479,
         4,    58,   1481, 0,    4,    135,  132,  500,  1484, 38,   582,  588,
         1,    6,    1484, 132,  1484, 1490, 0,    6,    132,  1,    1484, 1494,
         1,    4,    134,  135,  1494, 1498, 6,    38,   242,  0,    4,    242,
         6,    242,  1504, 0,    242,  500,  8,    500,  1116, 4,    58,   242,
         3,    6,    310,  312,  927,  1514, 1,    4,    354,  2,    7,    1518,
         5,    6,    354,  9,    1520, 1522, 3,    4,    242,  0,    7,    1526,
         9,    1348, 1528, 0,    3,    102,  1,    4,    102,  2,    7,    1534,
         9,    1532, 1536, 1,    6,    660,  312,  927,  1540, 0,    3,    1030,
         1,    6,    1030, 2,    5,    1546, 9,    1544, 1548, 1,    2,    1030,
         3,    6,    1030, 0,    5,    1554, 9,    1552, 1556, 1,    2,    102,
         3,    4,    102,  0,    7,    1562, 9,    1560, 1564, 4,    6,    355,
         6,    92,   1569, 8,    1568, 1571, 3,    6,    132,  7,    1568, 1574,
         6,    8,    93,   7,    1568, 1578, 3,    8,    554,  4,    7,    1582,
         4,    6,    1582, 6,    1584, 1587, 4,    146,  1569, 8,    1568, 1591,
         6,    358,  1569, 8,    1568, 1595, 2,    60,   1569, 8,    1568, 1599,
         4,    6,    354,  2,    1569, 1602, 8,    1568, 1605, 2,    926,  1569,
         8,    1568, 1609, 5,    6,    1582, 4,    1587, 1612, 8,    312,  927,
         6,    313,  1616, 302,  1616, 1618, 4,    8,    313,  5,    6,    1622,
         0,    9,    1624, 4,    312,  1626, 7,    1624, 1628, 4,    312,  1624,
         0,    9,    1632, 7,    1624, 1634, 2,    5,    310,  6,    310,  1638,
         0,    383,  1640, 0,    2,    383,  4,    6,    1644, 218,  383,  1646,
         0,    2,    346,  4,    8,    1651, 282,  347,  1652, 6,    8,    1651,
         302,  347,  1656, 7,    102,  312,  6,    313,  1660, 302,  1660, 1662,
         6,    102,  313,  302,  1660, 1666, 5,    312,  1030, 6,    313,  1670,
         302,  1670, 1672, 5,    6,    216,  0,    146,  1677, 4,    1676, 1679,
         6,    216,  267,  1,    38,   1682, 0,    5,    1146, 6,    8,    1686,
         147,  1146, 1688, 6,    9,    376,  0,    2,    1692, 376,  500,  1695,
         0,    2,    590,  267,  500,  1698, 2,    6,    376,  0,    9,    1702,
         376,  500,  1705, 0,    4,    146,  216,  500,  1709, 216,  500,  675,
         0,    4,    147,  102,  1146, 1714, 406,  520,  1030, 8,    377,  490,
         0,    9,    1720, 501,  1720, 1722, 4,    8,    58,   0,    1720, 1727,
         0,    8,    500,  0,    1720, 1731, 0,    577,  1720, 0,    4,    753,
         752,  1030, 1737, 0,    134,  1281, 6,    8,    357,  7,    1740, 1742,
         2,    6,    357,  0,    133,  1746, 7,    1742, 1748, 7,    138,  1742,
         6,    92,   377,  0,    8,    1754, 1,    8,    1754, 0,    1757, 1758,
         6,    8,    1737, 7,    752,  1762, 4,    9,    376,  483,  656,  1766,
         2,    9,    48,   475,  656,  1770, 6,    8,    217,  2,    5,    1774,
         0,    1677, 1776, 2,    7,    558,  0,    575,  1780, 2,    5,    560,
         0,    1479, 1784, 6,    8,    1527, 0,    1348, 1789, 2,    8,    39,
         2,    5,    38,   6,    8,    1794, 0,    1792, 1797, 2,    8,    59,
         2,    7,    58,   4,    8,    1802, 0,    1800, 1805, 3,    4,    656,
         312,  501,  1808, 312,  501,  1514, 6,    8,    377,  312,  501,  1814,
         4,    8,    217,  2,    7,    1818, 0,    1137, 1820, 61,   500,  1730,
         1,    8,    1802, 4,    58,   1826, 1,    8,    1794, 6,    38,   1830,
         0,    8,    60,   61,   500,  1834, 0,    9,    60,   4,    58,   1839,
         6,    38,   1839, 216,  432,  1113, 3,    216,  432,  61,   432,  1846,
         3,    60,   216,  61,   432,  1850, 5,    6,    48,   2,    7,    540,
         1,    1854, 1856, 2,    61,   216,  1,    1850, 1860, 51,   500,  924,
         2,    8,    1188, 267,  500,  1866, 0,    8,    1146, 5,    146,  1870,
         147,  1146, 1872, 0,    2,    61,   1,    1850, 1876, 4,    7,    376,
         6,    313,  376,  1,    1880, 1882, 3,    4,    282,  357,  1160, 1886,
         5,    58,   132,  59,   1838, 1890, 0,    5,    318,  8,    312,  1895,
         6,    318,  1897, 0,    2,    323,  9,    500,  1900, 322,  501,  1902,
         7,    38,   1830, 6,    1833, 1906, 5,    58,   1826, 4,    1829, 1910,
         0,    8,    501,  0,    2,    501,  9,    60,   1916, 1,    1914, 1918,
         4,    6,    1839, 8,    312,  1923, 1,    1838, 1924, 0,    9,    346,
         4,    6,    1929, 8,    312,  1931, 1,    1928, 1932, 6,    39,   1830,
         38,   1833, 1936, 4,    146,  197,  4,    146,  196,  0,    1940, 1943,
         2,    60,   197,  3,    1876, 1946, 4,    6,    41,   0,    3,    1950,
         0,    2,    1951, 197,  1952, 1954, 6,    196,  358,  6,    197,  358,
         0,    1959, 1960, 5,    6,    376,  0,    2,    1965, 6,    8,    1966,
         4,    376,  1969, 377,  1964, 1970, 2,    4,    382,  500,  1644, 1975,
         2,    4,    267,  0,    7,    1978, 8,    266,  1981, 0,    1978, 1982,
         6,    1980, 1985, 0,    10,   382,  6,    1058, 1989, 2,    48,   382,
         6,    416,  1993, 4,    8,    146,  6,    8,    147,  0,    2,    1999,
         1997, 1998, 2000, 6,    103,  312,  3,    1660, 2004, 4,    312,  1031,
         3,    1670, 2008, 2,    354,  927,  3,    354,  926,  9,    2012, 2014,
         9,    312,  926,  3,    1616, 2018, 3,    8,    2018, 927,  2018, 2022,
         2,    9,    2014, 927,  2014, 2026, 3,    6,    1660, 103,  1660, 2030,
         3,    4,    1670, 1031, 1670, 2034, 2,    9,    60,   2,    8,    60,
         0,    2038, 2041, 0,    432,  2041, 60,   1876, 2041, 0,    1146, 1997,
         0,    520,  1425, 358,  406,  1425, 146,  1714, 1997, 48,   134,  927,
         9,    1150, 1876, 3,    1876, 2038, 2,    60,   203,  0,    9,    338,
         2,    60,   2065, 6,    203,  358,  4,    146,  203,  2,    203,  1950,
         2,    4,    203,  6,    203,  2074, 8,    49,   60,   8,    146,  377,
         2,    41,   60,   1,    8,    2082, 2,    60,   339,  1,    8,    2086,
         5,    60,   358,  1,    8,    2090, 7,    60,   146,  1,    8,    2094,
         3,    40,   1030, 5,    202,  2098, 4,    8,    147,  5,    202,  2102,
         1,    8,    338,  0,    2041, 2106, 5,    8,    202,  2,    6,    2110,
         202,  2110, 2113, 5,    8,    40,   2,    6,    2116, 202,  2116, 2119,
         2,    4,    154,  154,  202,  2123, 7,    8,    202,  2,    4,    2126,
         202,  2126, 2129, 6,    8,    92,   0,    190,  2133, 0,    190,  1425,
         2,    6,    203,  132,  202,  2139, 1,    2,    1150, 1,    10,   14,
         1,    8,    26,   2,    8,    61,   1,    60,   2148, 1,    8,    1042,
         1,    146,  2102, 5,    8,    146,  1,    4,    2156, 1,    8,    2038,
         6,    9,    358,  1,    8,    2162, 1,    6,    12,   5,    8,    58,
         0,    3,    2168, 2,    1479, 2170, 8,    58,   2171, 2,    2170, 2175,
         6,    102,  1561, 2,    8,    2178, 0,    1560, 2181, 0,    2,    2169,
         1479, 2168, 2184, 1,    2,    2168, 0,    1479, 2188, 2,    9,    58,
         59,   2170, 2192, 5,    8,    2192, 0,    3,    2196, 59,   2192, 2198,
         5,    312,  346,  7,    8,    346,  346,  2202, 2204, 4,    7,    620,
         313,  602,  2208, 6,    102,  312,  4,    7,    2212, 313,  2212, 2214,
         4,    6,    501,  0,    2,    2218, 2,    9,    2218, 500,  2220, 2223,
         346,  602,  2204, 4,    313,  602,  602,  1030, 2228, 346,  602,  1030,
         4,    312,  1030, 313,  602,  2234, 60,   382,  555,  346,  605,  2202,
         2,    5,    408,  4,    359,  2242, 3,    6,    2156, 2,    147,  2246,
         8,    338,  2087, 8,    40,   807,  8,    40,   2083, 4,    41,   664,
         8,    40,   2257, 6,    41,   92,   8,    40,   2261, 2,    41,   926,
         8,    40,   2265, 8,    40,   1425, 8,    40,   787,  0,    9,    618,
         4,    312,  2273, 6,    619,  2274, 4,    7,    312,  303,  346,  2278,
         4,    203,  602,  4,    602,  2273, 203,  312,  346,  312,  346,  2273,
         4,    6,    2273, 312,  2273, 2290, 4,    6,    203,  203,  312,  2294,
         302,  312,  2279, 6,    2278, 2299, 6,    2273, 2278, 6,    8,    356,
         2,    5,    2304, 1,    48,   2306, 0,    2,    1306, 6,    1306, 2310,
         3,    10,   2312, 8,    10,   267,  0,    6,    2316, 10,   2316, 2318,
         0,    8,    490,  3,    4,    2322, 2,    5,    2322, 1,    2324, 2326,
         10,   660,  1964, 5,    6,    1188, 10,   660,  2332, 10,   544,  1306,
         1,    2,    48,   5,    8,    2338, 544,  2338, 2340, 10,   660,  1072,
         6,    8,    235,  2,    232,  2346, 4,    235,  2348, 2,    102,  232,
         3,    290,  2352, 3,    4,    232,  102,  290,  2356, 3,    232,  290,
         102,  290,  2360, 2,    5,    232,  6,    8,    2364, 2,    232,  2367,
         4,    2364, 2369, 2,    103,  232,  4,    2364, 2373, 2,    102,  233,
         102,  290,  2377, 233,  2352, 2356, 4,    2352, 2373, 3,    4,    2352,
         233,  2352, 2384, 2,    4,    58,   2,    560,  2389, 1,    4,    906,
         6,    906,  2392, 1,    4,    900,  6,    900,  2396, 1,    4,    910,
         6,    910,  2400, 1,    4,    914,  6,    914,  2404, 1,    4,    890,
         6,    890,  2408, 4,    890,  1328, 4,    7,    1328, 8,    1328, 2414,
         8,    103,  1328, 2,    6,    39,   5,    6,    38,   8,    2420, 2423,
         4,    7,    50,   4,    9,    50,   6,    2426, 2429, 5,    8,    346,
         312,  346,  2432, 4,    6,    51,   5,    8,    2436, 50,   2436, 2438,
         5,    6,    50,   8,    2436, 2442, 8,    346,  602,  0,    9,    10,
         2,    6,    11,   4,    2449, 2450, 4,    8,    50,   5,    6,    2454,
         51,   2454, 2456, 4,    8,    312,  5,    6,    2460, 313,  2460, 2462,
         2,    4,    628,  0,    10,   2467, 2,    4,    629,  0,    3,    2470,
         5,    2470, 2472, 2,    377,  628,  4,    376,  2477, 4,    49,   628,
         2,    48,   2481, 3,    376,  2470, 5,    48,   2470, 2,    4,    14,
         0,    10,   2489, 48,   376,  629,  0,    2467, 2470, 2,    5,    628,
         48,   629,  2496, 2,    8,    1854, 1,    48,   2500, 1,    48,   1478,
         3,    10,   1478, 3,    8,    10,   10,   58,   2508, 10,   58,   2193,
         4,    267,  1478, 0,    6,    267,  2,    8,    2516, 4,    267,  2518,
         1,    6,    1460, 2,    4,    2523, 1460, 2522, 2525, 0,    93,   1172,
         6,    9,    2528, 1172, 2528, 2531, 500,  523,  1188, 3,    6,    1876,
         4,    8,    1876, 1,    2536, 2538, 267,  424,  1460, 267,  424,  574,
         3,    6,    376,  1,    1460, 2546, 1,    1460, 1854, 5,    6,    746,
         1,    1460, 2552, 1,    574,  2546, 5,    8,    746,  302,  629,  2558,
         0,    9,    1514, 310,  927,  2562, 310,  927,  1838, 232,  357,  1298,
         357,  1030, 1838, 4,    9,    58,   0,    3,    2572, 5,    8,    2574,
         59,   2572, 2576, 0,    5,    1030, 1,    60,   1030, 9,    2580, 2582,
         0,    5,    322,  4,    7,    322,  9,    2586, 2588, 4,    9,    2170,
         59,   2168, 2592, 302,  322,  927,  6,    8,    1979, 1,    266,  2598,
         4,    14,   49,   6,    8,    2339, 4,    49,   2604, 4,    14,   465,
         2,    14,   377,  1,    2,    14,   4,    14,   2612, 1,    14,   266,
         1,    14,   444,  1,    8,    904,  1,    8,    500,  0,    5,    1424,
         217,  358,  2624, 6,    8,    216,  0,    5,    2628, 217,  358,  2630,
         4,    8,    521,  354,  358,  2635, 0,    3,    1424, 357,  358,  2638,
         0,    9,    146,  267,  358,  2642, 1,    4,    282,  2,    7,    2646,
         5,    1886, 2648, 4,    8,    267,  0,    6,    2653, 267,  358,  2654,
         6,    48,   629,  5,    358,  2658, 7,    146,  2658, 6,    48,   628,
         48,   146,  2665, 2,    283,  2646, 41,   282,  2668, 41,   282,  2648,
         282,  1259, 2648, 2,    4,    746,  282,  358,  2677, 4,    8,    216,
         60,   555,  2680, 2,    41,   1124, 8,    500,  2684, 4,    6,    1125,
         2,    1124, 2689, 8,    500,  2690, 5,    358,  1124, 8,    500,  2694,
         7,    146,  1124, 8,    500,  2698, 2,    5,    1124, 7,    1124, 2702,
         8,    500,  2704, 1,    58,   358,  8,    1166, 2708, 8,    41,   500,
         0,    2,    2712, 500,  2712, 2714, 1,    38,   146,  8,    1132, 2718,
         0,    2,    927,  4,    6,    2723, 8,    927,  2724, 2722, 2724, 2726,
         4,    7,    628,  974,  2470, 2731, 1,    2,    232,  267,  554,  2734,
         9,    232,  2736, 3,    232,  376,  4,    6,    232,  9,    376,  2742,
         1,    2740, 2744, 4,    6,    2740, 9,    376,  2748, 1,    2740, 2750,
         2,    5,    354,  1,    1602, 2754, 9,    232,  2756, 7,    354,  376,
         1,    6,    2760, 1766, 2760, 2762, 4,    282,  376,  3,    8,    2766,
         7,    376,  2768, 1,    2766, 2770, 9,    376,  554,  3,    8,    2774,
         7,    376,  2776, 1,    2774, 2778, 7,    8,    2774, 3,    376,  2782,
         1,    2774, 2784, 8,    38,   233,  48,   2734, 2789, 1,    60,   242,
         0,    2041, 2792, 0,    8,    2039, 2,    61,   2796, 3,    2038, 2798,
         9,    60,   1876, 3,    8,    2802, 61,   2802, 2804, 61,   1150, 2802,
         0,    2041, 2142, 1,    6,    408,  0,    1425, 2812, 0,    1997, 2158,
         8,    358,  1425, 0,    7,    2818, 6,    1425, 2820, 8,    146,  1997,
         0,    5,    2824, 4,    1997, 2826, 94,   927,  2448, 146,  629,  1544,
         41,   282,  1552, 8,    377,  1702, 0,    7,    266,  8,    266,  2839,
         0,    7,    92,   8,    92,   2843, 8,    242,  554,  4,    8,    1348,
         6,    8,    1336, 0,    6,    266,  1,    8,    2852, 8,    60,   242,
         8,    266,  656,  8,    242,  926,  0,    2,    102,  4,    283,  2862,
         102,  133,  2864, 3,    4,    134,  1,    2,    2868, 0,    7,    2868,
         5,    2870, 2872, 8,    2868, 2874, 1,    2,    1366, 0,    7,    1366,
         5,    2878, 2880, 8,    1366, 2882, 8,    38,   2878, 5,    1366, 2886,
         8,    2878, 2880, 5,    1366, 2890, 8,    38,   2870, 5,    2868, 2894,
         4,    9,    60,   0,    7,    2898, 8,    10,   2900, 5,    2898, 2902,
         3,    4,    26,   8,    10,   38,   5,    2906, 2908, 9,    10,   160,
         38,   160,  2912, 9,    10,   1066, 38,   1066, 2916, 10,   41,   50,
         8,    40,   2921, 5,    8,    554,  3,    6,    2924, 2,    555,  2924,
         4,    2926, 2928, 3,    4,    702,  2,    501,  702,  6,    2932, 2934,
         8,    10,   50,   8,    40,   2939, 8,    147,  500,  2,    6,    2942,
         501,  2942, 2944, 8,    359,  554,  2,    4,    2948, 555,  2948, 2950,
         1,    8,    1188, 4,    6,    1188, 359,  2954, 2956, 1,    8,    38,
         40,   573,  2960, 0,    5,    508,  0,    6,    509,  40,   2964, 2967,
         61,   226,  1818, 7,    134,  1532, 5,    8,    134,  0,    3,    2974,
         7,    134,  2976, 0,    665,  1560, 2,    665,  1532, 0,    2,    103,
         102,  665,  2984, 9,    972,  1532, 5,    6,    972,  0,    3,    2990,
         9,    972,  2992, 6,    8,    1533, 2,    1532, 2997, 0,    4,    95,
         3,    94,   3000, 6,    8,    3000, 2,    3002, 3005, 2,    4,    657,
         1,    656,  3008, 6,    8,    3008, 0,    3010, 3013, 0,    656,  3013,
         3008, 3013, 3016, 2,    94,   3005, 3000, 3005, 3020, 0,    656,  3009,
         3008, 3013, 3024, 2,    94,   3001, 3000, 3005, 3028, 6,    8,    3029,
         3000, 3028, 3033, 6,    8,    3025, 3008, 3024, 3037, 7,    8,    3000,
         9,    3028, 3040, 7,    8,    3008, 9,    3024, 3044, 216,  267,  500,
         1,    1166, 1478, 10,   58,   313,  3,    4,    216,  1,    1676, 3054,
         313,  376,  500,  1,    4,    1090, 2,    9,    358,  1090, 3060, 3062,
         0,    4,    3062, 1,    1090, 3066, 0,    4,    94,   6,    94,   3071,
         0,    8,    3072, 4,    3071, 3074, 1,    8,    358,  359,  3066, 3078,
         2,    9,    3078, 0,    4,    3082, 359,  3078, 3084, 1,    4,    94,
         5,    6,    3088, 0,    8,    3090, 95,   3088, 3092, 0,    8,    358,
         8,    3066, 3097, 1,    8,    3066, 359,  3066, 3100, 354,  734,  1133,
         2,    8,    501,  0,    3,    3106, 1,    2,    3108, 3107, 3108, 3110,
         217,  1116, 1914, 0,    2,    228,  0,    8,    229,  217,  3116, 3118,
         354,  1116, 1731, 0,    9,    504,  1,    8,    3124, 505,  3124, 3126,
         3,    8,    500,  0,    501,  3130, 1,    500,  3132, 3131, 3132, 3134,
         312,  1914, 1917, 2,    6,    38,   354,  577,  3140, 354,  1727, 2388,
         0,    2082, 2255, 0,    2,    661,  5,    6,    3148, 4,    7,    3148,
         3,    3150, 3152, 0,    2,    2103, 4,    7,    3156, 3,    146,  3158,
         4,    7,    2000, 3,    146,  3162, 4,    8,    359,  0,    2,    3167,
         5,    6,    3168, 3,    358,  3170, 6,    8,    359,  0,    2,    3175,
         5,    6,    3176, 3,    358,  3178, 0,    2,    1151, 4,    7,    3182,
         5,    60,   3184, 5,    6,    3182, 7,    60,   3188, 5,    60,   3152,
         7,    60,   3150, 355,  2012, 2014, 4,    313,  1030, 5,    2008, 3198,
         7,    1666, 2004, 1030, 2008, 2235, 6,    1660, 2213, 2,    9,    926,
         0,    3,    3208, 1,    8,    3208, 927,  3210, 3212, 5,    8,    312,
         618,  621,  3216, 312,  2235, 3198, 312,  1666, 2213, 0,    243,  926,
         0,    242,  926,  242,  3224, 3227, 3,    6,    10,   8,    10,   3230,
         6,    10,   135,  8,    10,   973,  3,    10,   664,  4,    267,  664,
         1,    48,   664,  0,    7,    164,  41,   164,  3244, 11,   38,   134,
         11,   904,  1188, 38,   661,  746,  0,    151,  172,  0,    157,  164,
         4,    8,    60,   0,    2898, 3259, 58,   266,  665,  0,    5,    60,
         8,    60,   3265, 4,    3264, 3267, 2,    151,  1040, 1,    40,   1996,
         1,    2,    926,  8,    40,   3274, 1,    2,    1950, 8,    40,   3278,
         8,    40,   432,  6,    10,   190,  6,    190,  358,  1,    4,    664,
         8,    40,   3288, 8,    40,   1146, 41,   252,  1172, 232,  2428, 2455,
         5,    50,   232,  4,    9,    3298, 51,   3298, 3300, 4,    51,   232,
         9,    3298, 3304, 5,    8,    50,   9,    3304, 3308, 4,    8,    51,
         9,    3298, 3312, 4,    50,   232,  232,  2428, 3317, 0,    7,    3308,
         4,    51,   3320, 9,    3308, 3322, 0,    7,    3312, 5,    50,   3326,
         9,    3312, 3328, 4,    2455, 3298, 1,    746,  2680, 1,    2,    218,
         8,    490,  3337, 8,    746,  1159, 2,    8,    1316, 3,    490,  3342,
         4,    8,    1072, 3,    490,  3346, 1,    216,  630,  3,    6,    2680,
         1,    216,  3352, 1,    6,    2680, 3,    216,  3356, 3,    490,  2680,
         0,    8,    1302, 1,    746,  3362, 0,    41,   1042, 0,    339,  2038,
         0,    41,   2162, 0,    41,   1048, 2,    9,    1950, 0,    41,   3374,
         0,    41,   2038, 0,    26,   41,   5,    8,    266,  2,    614,  3383,
         0,    383,  3384, 0,    7,    3274, 2,    628,  926,  6,    3388, 3391,
         0,    6,    3275, 3274, 3391, 3394, 0,    146,  927,  665,  3274, 3398,
         0,    2,    926,  6,    926,  3403, 1,    2,    3404, 6,    8,    3402,
         0,    3406, 3409, 0,    3,    3404, 2,    3409, 3412, 0,    2,    3405,
         3404, 3409, 3416, 4,    8,    266,  6,    267,  3420, 1,    2,    3422,
         0,    383,  3424, 9,    3274, 3388, 2,    926,  3429, 6,    3388, 3431,
         2,    746,  927,  665,  3274, 3434, 1,    2,    2156, 0,    151,  3438,
         9,    590,  1532, 9,    102,  266,  7,    1532, 3444, 0,    5,    94,
         9,    94,   266,  7,    3448, 3450, 9,    590,  3448, 7,    102,  266,
         9,    1532, 3456, 7,    94,   266,  9,    3448, 3460, 2991, 2992, 2994,
         9,    972,  2990, 2991, 2992, 3466, 2,    5,    926,  6,    972,  3471,
         0,    927,  3472, 8,    2843, 3000, 8,    625,  3008, 1,    6,    624,
         2,    4,    3481, 8,    625,  3482, 3,    6,    2842, 0,    4,    3487,
         8,    2843, 3488, 8,    591,  1978, 2,    267,  3258, 4,    150,  267,
         10,   146,  660,  3,    4,    18,   5,    10,   3500, 3,    4,    664,
         5,    10,   3504, 2,    4,    383,  267,  382,  3508, 1,    376,  3504,
         2,    267,  3504, 3,    4,    382,  2,    267,  3516, 2,    58,   357,
         7,    356,  3520, 60,   3520, 3522, 0,    8,    48,   2,    7,    3526,
         60,   541,  3528, 5,    312,  432,  60,   1398, 3532, 3,    146,  232,
         102,  232,  3537, 2,    3536, 3539, 1,    2,    302,  4,    6,    3542,
         302,  500,  3543, 2,    3545, 3546, 3,    302,  500,  4,    6,    3551,
         302,  500,  3552, 2,    3550, 3555, 6,    61,   356,  2,    58,   3559,
         356,  3559, 3560, 3,    58,   356,  4,    6,    3565, 5,    356,  3566,
         2,    3564, 3569, 58,   356,  3566, 2,    3564, 3573, 4,    8,    282,
         2,    6,    3576, 3,    282,  926,  2,    3579, 3580, 0,    904,  927,
         5,    38,   904,  6,    38,   559,  4,    58,   561,  4,    58,   927,
         6,    38,   927,  0,    500,  927,  0,    555,  904,  9,    38,   58,
         4,    9,    312,  7,    1624, 3602, 4,    8,    2450, 0,    396,  3607,
         7,    10,   660,  5,    2448, 3610, 3,    10,   1030, 5,    2448, 3614,
         9,    712,  3216, 9,    312,  1622, 7,    1624, 3620, 7,    8,    2448,
         3,    10,   3624, 5,    2448, 3626, 3,    8,    2448, 7,    10,   3630,
         5,    2448, 3632, 6,    313,  3216, 4,    7,    3636, 9,    3216, 3638,
         7,    8,    3602, 5,    312,  3642, 313,  3602, 3644, 0,    634,  1031,
         0,    634,  1030, 6,    3649, 3650, 0,    635,  1030, 636,  1030, 3655,
         4,    8,    640,  0,    634,  3659, 6,    640,  3661, 6,    640,  3649,
         1,    636,  3650, 635,  644,  3650, 636,  644,  1030, 6,    959,  3650,
         4,    8,    959,  0,    634,  3674, 6,    959,  3676, 347,  348,  1928,
         0,    322,  2305, 0,    322,  577,  0,    8,    346,  0,    348,  3687,
         8,    1928, 3687, 5,    6,    310,  7,    1838, 3692, 60,   1382, 1835,
         4,    6,    242,  282,  310,  3699, 302,  656,  3699, 60,   1835, 2580,
         92,   282,  2467, 2,    4,    656,  8,    40,   3709, 0,    656,  3711,
         8,    359,  3008, 0,    656,  3715, 8,    266,  358,  267,  282,  3718,
         8,    267,  282,  282,  358,  3722, 8,    266,  359,  0,    656,  3727,
         0,    6,    92,   2,    4,    3730, 92,   282,  3733, 10,   282,  291,
         2,    4,    522,  282,  358,  3739, 0,    3,    656,  927,  3008, 3742,
         0,    10,   657,  19,   656,  3746, 0,    10,   103,  19,   102,  3750,
         0,    10,   95,   19,   94,   3754, 0,    10,   15,   14,   19,   3758,
         6,    8,    3758, 14,   3758, 3763, 358,  1425, 3448, 2,    4,    95,
         6,    8,    3768, 3448, 3768, 3771, 6,    8,    634,  634,  3448, 3775,
         2,    4,    3449, 6,    8,    3778, 3448, 3778, 3781, 0,    5,    614,
         4,    7,    614,  9,    3784, 3786, 6,    8,    2984, 102,  302,  3791,
         4,    8,    3403, 282,  927,  3794, 6,    8,    3403, 302,  927,  3798,
         218,  383,  904,  6,    218,  267,  9,    222,  3804, 102,  302,  383,
         2,    4,    731,  6,    8,    3810, 38,   730,  3813, 0,    6,    376,
         4,    8,    376,  1030, 3816, 3819, 0,    665,  1030, 5,    666,  3822,
         5,    50,   354,  4,    7,    3826, 9,    3826, 3828, 4,    7,    354,
         5,    2428, 3832, 7,    1522, 2428, 7,    904,  3826, 0,    2,    904,
         5,    354,  3840, 7,    904,  3842, 4,    242,  1189, 0,    927,  3846,
         1,    6,    376,  102,  1766, 3851, 3,    8,    904,  0,    7,    3854,
         4,    6,    3854, 904,  3856, 3859, 4,    7,    746,  3,    8,    3862,
         2,    8,    3862, 2,    3864, 3867, 3,    8,    640,  634,  3659, 3870,
         3,    4,    1188, 2,    8,    3875, 2,    8,    3874, 3874, 3876, 3879,
         2,    9,    3874, 8,    3879, 3882, 2,    8,    1189, 3,    4,    3886,
         5,    1188, 3886, 9,    3888, 3890, 4,    8,    1189, 2,    5,    3894,
         3,    1188, 3894, 9,    3896, 3898, 3,    8,    1188, 2,    5,    3902,
         4,    1189, 3902, 9,    3904, 3906, 5,    8,    1188, 3,    4,    3910,
         2,    1189, 3910, 9,    3912, 3914, 4,    9,    1876, 5,    8,    1876,
         1877, 3918, 3920, 5,    8,    3918, 1877, 3918, 3924, 5,    378,  3818,
         1,    6,    10,   8,    394,  3930, 1,    4,    746,  2,    5,    746,
         8,    3934, 3936, 8,    432,  3264, 58,   92,   313,  0,    8,    10,
         1,    394,  3944, 3,    366,  420,  11,   3930, 3944, 49,   420,  544,
         2,    8,    544,  49,   544,  3954, 1,    6,    3106, 4,    9,    3958,
         3106, 3130, 3960, 0,    8,    555,  4,    6,    555,  2,    3964, 3966,
         2,    3965, 3966, 8,    3969, 3970, 0,    7,    3130, 5,    8,    3974,
         500,  3131, 3976, 2,    3130, 3979, 4,    6,    3106, 1,    2,    3982,
         9,    500,  3984, 3,    3106, 3986, 1,    2,    2218, 9,    500,  3990,
         3,    3106, 3992, 1,    2,    904,  9,    500,  3996, 3,    3106, 3998,
         1,    4,    3106, 9,    500,  3106, 6,    4002, 4004, 3,    3106, 4006,
         4,    3958, 4004, 3,    3106, 4010, 1,    4,    4004, 6,    4004, 4014,
         3,    3106, 4016, 3,    8,    3966, 3964, 3966, 4021, 2,    4020, 4023,
         303,  926,  2984, 6,    8,    303,  0,    2,    4029, 303,  926,  4030,
         1,    4,    2984, 5,    6,    2984, 8,    4034, 4036, 0,    2,    1031,
         1,    6,    4040, 4,    7,    4040, 8,    4042, 4044, 2,    38,   103,
         39,   576,  4048, 6,    8,    4048, 39,   4048, 4052, 4,    8,    59,
         2,    6,    4057, 59,   1726, 4058, 4,    8,    4058, 59,   4058, 4062,
         39,   576,  3810, 0,    3,    40,   8,    1950, 4069, 0,    3,    338,
         8,    60,   4073, 8,    60,   4069, 0,    3,    926,  8,    60,   4079,
         8,    60,   3071, 0,    6,    660,  8,    60,   4085, 0,    6,    48,
         8,    60,   4089, 2,    5,    60,   0,    6,    4093, 8,    60,   4095,
         60,   490,  905,  51,   146,  926,  41,   490,  926,  8,    60,   490,
         6,    92,   313,  217,  502,  3106, 312,  1150, 1835, 312,  1731, 3130,
         3,    8,    346,  312,  3687, 4114, 2,    9,    500,  217,  1914, 4118,
         0,    8,    61,   217,  2038, 4122, 0,    8,    3931, 0,    9,    3930,
         1,    4126, 4128, 0,    8,    433,  0,    9,    432,  1,    4132, 4134,
         0,    8,    1147, 0,    9,    1146, 1,    4138, 4140, 0,    8,    521,
         0,    9,    520,  1,    4144, 4146, 4,    6,    48,   1,    132,  4150,
         3,    4,    50,   1,    132,  4154, 1,    4,    132,  60,   132,  4158,
         0,    133,  1188, 4,    132,  4163, 4,    6,    491,  1,    132,  4166,
         0,    2,    1030, 8,    10,   4171, 0,    4,    972,  8,    10,   4175,
         1,    132,  3258, 132,  1189, 4158, 2,    7,    376,  4,    8,    4183,
         1,    376,  4184, 0,    1731, 2622, 8,    38,   611,  6,    610,  4191,
         8,    577,  734,  302,  656,  927,  9,    610,  730,  39,   610,  734,
         6,    9,    610,  39,   610,  4202, 7,    730,  734,  4,    8,    243,
         60,   1340, 4209, 0,    8,    3275, 500,  927,  4212, 927,  3584, 3854,
         0,    3,    906,  5,    6,    4218, 7,    904,  4220, 0,    5,    1578,
         4,    927,  4224, 0,    5,    3174, 4,    927,  4228, 0,    7,    2102,
         6,    927,  4232, 1,    4,    1578, 0,    927,  4236, 1,    6,    2102,
         0,    927,  4240, 1,    4,    3174, 0,    927,  4244, 0,    8,    3997,
         5,    6,    4248, 7,    904,  4250, 2,    9,    554,  4,    146,  4255,
         6,    358,  4255, 2,    60,   4255, 2,    8,    554,  60,   555,  4262,
         60,   555,  2040, 8,    60,   1583, 282,  358,  3067, 3,    8,    282,
         0,    4,    4273, 282,  358,  4275, 2,    7,    3420, 267,  282,  4278,
         2,    7,    3576, 267,  282,  4282, 1,    2,    3576, 41,   282,  4286,
         4,    8,    40,   1,    2,    4290, 41,   282,  4292, 2,    9,    10,
         4,    6,    4296, 10,   282,  4299, 218,  554,  629,  302,  501,  656,
         282,  310,  501,  59,   218,  282,  39,   232,  302,  0,    9,    926,
         1,    8,    4312, 927,  4312, 4314, 1,    6,    1382, 103,  1382, 4318,
         1,    4,    2580, 1031, 2580, 4322, 0,    558,  577,  6,    8,    311,
         0,    3692, 4329, 38,   102,  927,  0,    5,    1546, 9,    1030, 4334,
         0,    9,    1546, 5,    1030, 4338, 0,    4,    103,  6,    9,    4342,
         7,    102,  4344, 0,    7,    1534, 9,    102,  4348, 0,    6,    1031,
         5,    8,    4352, 9,    1030, 4354, 4,    9,    4352, 5,    1030, 4358,
         0,    9,    1534, 7,    102,  4362, 7,    8,    4342, 9,    102,  4366,
         6,    8,    927,  1,    4,    4370, 0,    927,  4372, 2,    8,    1950,
         1,    40,   4376, 0,    41,   4376, 4377, 4378, 4380, 0,    338,  2040,
         0,    338,  2041, 2040, 4385, 4386, 1,    40,   2132, 0,    40,   2132,
         0,    4390, 4393, 1,    40,   1424, 0,    40,   1424, 0,    4396, 4399,
         0,    41,   2132, 40,   4393, 4402, 0,    41,   1424, 40,   4399, 4406,
         1,    338,  2040, 338,  2040, 4411, 0,    4410, 4413, 2133, 4390, 4402,
         1425, 4396, 4406, 0,    41,   4390, 2133, 4390, 4420, 1,    8,    282,
         2,    4,    4425, 2,    4,    4424, 7,    282,  4428, 4424, 4426, 4431,
         1,    628,  3008, 5,    1808, 4434, 6,    8,    629,  3,    4,    4438,
         2,    4,    4439, 1,    628,  4442, 5,    4440, 4444, 3,    4,    4424,
         6,    283,  4426, 5,    4448, 4450, 2,    5,    4424, 3,    4450, 4454,
         4,    4431, 4454, 2,    5,    656,  7,    282,  3708, 4,    4460, 4463,
         2,    4431, 4448, 2,    5,    4438, 3,    4444, 4468, 4439, 4440, 4468,
         1,    628,  4472, 0,    3,    4460, 4,    7,    4460, 9,    4476, 4478,
         1,    2,    3448, 4,    7,    4482, 9,    3448, 4484, 0,    5,    1454,
         9,    1336, 4488, 0,    5,    1808, 2,    7,    1808, 9,    4492, 4494,
         9,    1336, 3448, 2,    926,  2389, 2,    6,    266,  2,    926,  4503,
         2,    926,  3141, 2,    926,  1117, 2,    926,  3841, 905,  926,  3996,
         4,    6,    3997, 905,  3996, 4514, 1,    926,  1916, 2,    6,    267,
         4,    7,    4520, 8,    4520, 4522, 4,    7,    3850, 8,    3850, 4526,
         0,    93,   358,  0,    41,   634,  1,    4,    376,  8,    2546, 4534,
         8,    10,   2546, 8,    10,   2516, 8,    10,   1854, 8,    10,   2552,
         5,    6,    464,  8,    10,   4546, 8,    10,   406,  0,    6,    93,
         8,    10,   4552, 0,    6,    445,  8,    10,   4556, 3,    6,    454,
         8,    10,   4560, 0,    5,    2162, 8,    359,  4564, 7,    2162, 4566,
         7,    312,  660,  5,    6,    4570, 9,    4570, 4572, 3,    38,   972,
         9,    2990, 4576, 3,    58,   132,  9,    1372, 4580, 8,    38,   147,
         9,    38,   146,  5,    4584, 4586, 8,    58,   359,  9,    58,   358,
         7,    4590, 4592, 2,    4,    59,   8,    58,   4597, 9,    58,   4596,
         7,    4598, 4600, 8,    38,   2421, 9,    38,   2420, 5,    4604, 4606,
         48,   629,  2156, 376,  629,  1562, 376,  629,  1150, 232,  267,  1042,
         267,  282,  1372, 2,    7,    660,  267,  282,  4620, 232,  267,  2038,
         267,  282,  408,  267,  282,  1054, 232,  267,  2162, 1,    4,    216,
         6,    8,    4632, 4,    8,    3850, 4,    8,    2420, 4,    8,    4520,
         6,    8,    4596, 8,    926,  3274, 5,    6,    10,   4,    8,    4646,
         6,    8,    884,  1,    216,  926,  8,    10,   926,  4,    8,    93,
         0,    2,    4657, 2133, 4656, 4658, 8,    927,  2722, 3,    634,  4662,
         4,    93,   4662, 0,    2,    2133, 8,    2133, 4668, 4,    93,   4670,
         0,    4,    665,  8,    665,  4674, 5,    634,  4676, 0,    665,  1254,
         5,    634,  4680, 0,    8,    635,  3,    4,    4684, 634,  927,  4686,
         0,    927,  1254, 3,    634,  4690, 4,    665,  4684, 5,    634,  4694,
         5,    972,  3148, 9,    660,  4698, 0,    9,    554,  0,    500,  4703,
         1,    58,   2730, 58,   1030, 2581, 6,    38,   4703, 0,    5,    500,
         500,  1030, 4712, 0,    7,    500,  102,  500,  4716, 1,    6,    38,
         38,   102,  4720, 5,    6,    356,  1,    38,   4724, 8,    500,  559,
         38,   303,  500,  6,    8,    103,  4,    102,  4733, 4,    102,  927,
         6,    927,  1030, 9,    102,  1030, 8,    904,  927,  5,    904,  1030,
         6,    1030, 4079, 0,    3,    4746, 926,  4746, 4748, 3,    2722, 3274,
         6,    1030, 4753, 2723, 3402, 4738, 1,    2,    4738, 0,    3,    4758,
         926,  4758, 4760, 3,    3402, 4758, 0,    3,    4738, 1,    3402, 4766,
         6,    1030, 3275, 1,    3402, 4770, 3,    3402, 4746, 2,    346,  635,
         0,    4,    2041, 60,   2040, 4779, 0,    2,    1997, 146,  1996, 4783,
         5,    92,   346,  8,    146,  3934, 2,    5,    346,  8,    346,  4790,
         49,   60,   420,  49,   60,   2040, 92,   313,  602,  5,    6,    92,
         92,   313,  4800, 4,    8,    1346, 242,  904,  4805, 0,    1347, 4806,
         0,    3,    2622, 1188, 1731, 4810, 0,    1189, 3130, 1188, 1731, 4814,
         1,    242,  500,  6,    8,    500,  0,    243,  4820, 4818, 4821, 4822,
         0,    4,    2039, 2,    6,    4826, 2038, 4122, 4829, 51,   904,  972,
         5,    302,  4832, 8,    50,   500,  0,    4818, 4837, 5,    310,  746,
         7,    2162, 4840, 1,    4,    1348, 9,    1348, 4844, 6,    242,  4847,
         0,    4844, 4849, 0,    3,    904,  4,    6,    972,  0,    8,    4854,
         972,  4852, 4857, 133,  146,  232,  282,  358,  635,  60,   232,  661,
         41,   92,   282,  1,    2,    346,  312,  348,  4869, 0,    7,    1574,
         1,    6,    4872, 1575, 4872, 4874, 0,    4,    973,  49,   974,  4878,
         0,    5,    2102, 1,    4,    4882, 2103, 4882, 4884, 354,  1112, 1835,
         0,    2,    1602, 0,    8,    1602, 354,  4890, 4893, 354,  4079, 4312,
         0,    3,    1602, 0,    9,    1602, 354,  4899, 4900, 0,    9,    1996,
         1,    8,    4904, 1997, 4904, 4906, 0,    147,  2156, 1,    146,  4910,
         2157, 4910, 4912, 4,    242,  1031, 0,    5,    4916, 1030, 4916, 4918,
         8,    927,  3274, 9,    926,  3274, 0,    4922, 4924, 0,    2,    559,
         1,    576,  4928, 0,    2,    561,  1,    1726, 4932, 9,    576,  1830,
         0,    927,  3208, 1,    8,    4938, 926,  4938, 4940, 1,    8,    2722,
         0,    9,    4944, 926,  4944, 4946, 0,    9,    4922, 926,  4922, 4950,
         2,    8,    4313, 0,    9,    4954, 926,  4954, 4956, 0,    358,  656,
         8,    3008, 4961, 0,    358,  635,  8,    640,  4965, 6,    10,   635,
         8,    644,  4969, 283,  634,  1090, 14,   283,  634,  6,    10,   232,
         8,    290,  4977, 2,    8,    2646, 41,   282,  4980, 282,  635,  2648,
         6,    8,    2278, 6,    8,    2279, 2278, 4987, 4988, 6,    313,  1030,
         9,    1670, 4992, 604,  927,  1622, 2,    4,    354,  2,    7,    354,
         904,  4999, 5000, 904,  1340, 1505, 9,    312,  346,  8,    313,  346,
         347,  5006, 5008, 8,    313,  5006, 347,  5006, 5012, 4,    7,    3216,
         9,    3636, 5016, 6,    9,    2278, 7,    8,    5020, 2279, 5020, 5022,
         7,    312,  1622, 9,    1624, 5026, 58,   283,  1498, 2,    4,    103,
         0,    7,    5032, 1,    6,    5032, 102,  5034, 5036, 1,    6,    5034,
         102,  5034, 5040, 2,    6,    1031, 0,    5,    5044, 1,    4,    5044,
         1030, 5046, 5048, 1,    4,    5046, 1030, 5046, 5052, 5,    6,    640,
         1,    3658, 5056, 356,  555,  644,  555,  628,  1498, 1,    4,    2192,
         58,   283,  5064, 0,    5,    4118, 283,  500,  5068, 0,    103,  972,
         1,    6,    5072, 102,  5072, 5074, 7,    312,  356,  1,    4724, 5078,
         0,    2,    657,  303,  500,  5082, 1,    102,  972,  6,    5072, 5086,
         9,    356,  972,  1,    4724, 5090, 9,    356,  624,  1,    4724, 5094,
         0,    6,    5086, 103,  5086, 5098, 9,    58,   1188, 1,    1726, 5102,
         1,    4,    972,  4,    628,  972,  0,    5106, 5109, 0,    5,    972,
         629,  4878, 5112, 4,    629,  972,  5,    4878, 5116, 4,    628,  4879,
         972,  4878, 5121, 6,    8,    5107, 4,    972,  5124, 0,    5106, 5127,
         5,    972,  4878, 629,  4878, 5130, 5,    628,  972,  629,  4878, 5134,
         0,    4175, 5116, 6,    8,    4174, 4,    972,  5141, 0,    4175, 5142,
         4,    58,   312,  2,    1166, 5147, 3,    216,  228,  1,    2,    5150,
         229,  5150, 5152, 2,    3117, 5150, 8,    501,  1126, 1124, 1126, 5158,
         1124, 1126, 3106, 8,    500,  1125, 8,    1126, 5165, 9,    500,  1124,
         1124, 1126, 5169, 503,  1124, 1126, 0,    2,    735,  1,    1132, 5174,
         0,    2,    2573, 1,    1166, 5178, 0,    3,    664,  0,    4,    664,
         2470, 5182, 5185, 1,    2,    382,  0,    4,    383,  1975, 5188, 5190,
         0,    3,    382,  0,    4,    382,  3508, 5194, 5197, 4,    376,  382,
         4,    376,  383,  382,  5201, 5202, 2,    48,   383,  382,  1993, 5206,
         1,    2,    628,  2467, 4674, 5210, 6,    8,    5210, 0,    4,    5215,
         2467, 5210, 5216, 6,    8,    2466, 0,    4,    5221, 2467, 5210, 5222,
         4,    58,   303,  6,    38,   303,  0,    303,  500,  8,    311,  500,
         8,    58,   219,  6,    356,  555,  6,    303,  356,  1,    58,   356,
         5,    356,  500,  4,    9,    588,  0,    7,    5244, 582,  588,  5246,
         6,    132,  134,  1,    4,    5250, 132,  1484, 5252, 5,    628,  634,
         135,  1498, 5256, 4,    135,  628,  5,    134,  628,  0,    2,    5262,
         1,    5260, 5264, 7,    500,  580,  267,  1730, 5268, 2,    9,    1730,
         7,    500,  5272, 267,  1730, 5274, 2,    9,    576,  1,    38,   5278,
         267,  576,  5280, 0,    2,    310,  572,  576,  5285, 6,    9,    132,
         2,    4,    5289, 0,    3,    5290, 1,    4,    5288, 132,  5292, 5294,
         0,    6,    581,  4,    267,  5298, 9,    266,  5298, 580,  5300, 5303,
         4,    7,    200,  1,    2,    5306, 8,    40,   5309, 6,    5306, 5311,
         512,  656,  927,  8,    40,   2735, 4,    236,  5317, 8,    40,   1553,
         0,    1546, 5321, 4,    243,  1188, 7,    8,    5324, 6,    8,    5324,
         6,    5326, 5329, 0,    2,    905,  6,    660,  5332, 0,    2620, 5335,
         8,    5324, 5327, 6,    5326, 5339, 6,    8,    5325, 5324, 5329, 5342,
         4,    216,  746,  232,  904,  5347, 4,    8,    746,  228,  232,  5351,
         0,    5,    3854, 0,    6,    3854, 904,  5354, 5357, 0,    5,    660,
         904,  4085, 5360, 0,    4,    3854, 904,  3856, 5365, 5,    6,    660,
         6,    634,  5361, 7,    5368, 5370, 7,    8,    92,   6,    9,    92,
         1,    634,  5376, 93,   5374, 5378, 6,    9,    5374, 1,    634,  5382,
         93,   5374, 5384, 8,    93,   644,  7,    5376, 5388, 201,  408,  3174,
         9,    40,   520,  7,    3174, 5394, 3,    8,    634,  4,    7,    5398,
         6,    5399, 5400, 1,    634,  5402, 5,    5400, 5404, 5,    8,    634,
         2,    7,    5408, 6,    5409, 5410, 1,    634,  5412, 3,    5410, 5414,
         9,    92,   644,  7,    1578, 5418, 0,    1352, 1915, 0,    2,    311,
         1,    1730, 5424, 1,    1726, 5424, 2,    9,    2304, 1,    4,    5430,
         5,    2304, 5432, 2,    9,    1726, 1,    4,    5436, 5,    1726, 5438,
         1,    356,  5430, 5,    2304, 5442, 5,    356,  5430, 1,    2304, 5446,
         2,    9,    356,  5,    628,  5450, 1,    356,  5452, 1,    356,  5256,
         2,    4,    219,  5,    2304, 5458, 356,  500,  4151, 4,    8,    5082,
         5,    500,  5464, 7,    8,    242,  0,    4,    5468, 5,    500,  5470,
         7,    8,    490,  0,    4,    5474, 5,    500,  5476, 2,    8,    51,
         0,    4,    5480, 5,    500,  5482, 4,    61,   1726, 1,    58,   5486,
         4,    61,   1834, 1,    58,   5490, 4,    61,   64,   1,    58,   5494,
         5,    8,    500,  1,    2,    5498, 7,    5498, 5500, 0,    500,  5502,
         6,    40,   357,  356,  555,  5506, 8,    10,   41,   8,    10,   40,
         40,   5510, 5513, 358,  3719, 3726, 9,    266,  358,  267,  3726, 5518,
         8,    11,   40,   9,    10,   40,   41,   5522, 5524, 9,    10,   5522,
         41,   5522, 5528, 8,    267,  358,  359,  5518, 5532, 9,    266,  5532,
         359,  5532, 5536, 8,    38,   1189, 9,    38,   1188, 39,   5540, 5542,
         9,    1188, 5540, 39,   5540, 5546, 0,    2467, 3708, 0,    665,  926,
         0,    664,  926,  664,  5552, 5555, 0,    664,  927,  1,    5552, 5558,
         0,    359,  634,  1,    4964, 5562, 0,    18,   383,  1,    358,  634,
         359,  4964, 5568, 635,  5562, 5568, 1,    358,  5562, 635,  5562, 5574,
         0,    9,    1348, 1526, 3699, 5578, 1,    8,    312,  4,    6,    5583,
         3,    5582, 5584, 7,    312,  5586, 5,    5584, 5588, 5,    312,  5586,
         7,    5584, 5592, 3,    242,  1342, 5,    312,  5596, 7,    1342, 5598,
         5,    312,  1454, 243,  1336, 5602, 7,    312,  5596, 5,    1342, 5606,
         7,    312,  1526, 243,  1348, 5610, 5,    6,    5582, 3,    4,    5582,
         7,    312,  5616, 5583, 5614, 5618, 2,    6,    3078, 5,    6,    3078,
         522,  5623, 5624, 0,    9,    3078, 5623, 5624, 5628, 2,    4,    19,
         1,    14,   5632, 6,    8,    3709, 1,    3008, 5636, 1,    14,   3008,
         2,    8,    2853, 6,    216,  2853, 4,    5642, 5644, 9,    60,   216,
         4,    6,    5649, 216,  1113, 5650, 4,    7,    930,  102,  932,  5654,
         4,    7,    48,   102,  932,  5658, 932,  1030, 1854, 4,    8,    1854,
         1,    2,    5664, 1030, 1854, 5666, 4,    8,    2546, 1,    2,    5670,
         1030, 2546, 5672, 8,    48,   1854, 1,    2,    5676, 1030, 1854, 5678,
         0,    3,    482,  4,    7,    5682, 1,    376,  5684, 8,    482,  5686,
         3,    216,  3274, 4,    6,    3274, 927,  5690, 5692, 376,  629,  3070,
         376,  629,  4078, 2,    267,  926,  0,    383,  5700, 5,    10,   94,
         0,    15,   5704, 2,    629,  926,  0,    2467, 5708, 4,    95,   628,
         0,    2470, 5713, 8,    629,  1258, 282,  1259, 5716, 1,    6,    2740,
         9,    2740, 5720, 9,    232,  5720, 1,    6,    3536, 9,    232,  5726,
         8,    282,  1259, 0,    7,    5730, 1,    282,  5732, 0,    40,   232,
         8,    233,  5736, 6,    232,  5739, 0,    232,  634,  8,    233,  5742,
         6,    232,  5745, 0,    232,  290,  8,    233,  5748, 6,    232,  5751,
         5,    60,   232,  1,    6,    5754, 9,    232,  5756, 1,    232,  282,
         2,    5,    282,  3,    5760, 5762, 2,    8,    395,  4,    9,    394,
         11,   5766, 5768, 3,    8,    746,  266,  5351, 5772, 3,    8,    58,
         266,  1727, 5776, 3,    8,    2516, 4,    8,    2516, 266,  5780, 5783,
         2,    8,    746,  266,  2558, 5787, 266,  1479, 2168, 5,    8,    2516,
         266,  2519, 5792, 2,    8,    747,  11,   1298, 5796, 11,   1800, 2572,
         2,    9,    746,  4,    8,    747,  11,   5802, 5804, 628,  3071, 3088,
         102,  3000, 3088, 4,    94,   628,  628,  3088, 5813, 0,    94,   102,
         4,    3071, 5816, 6,    8,    3448, 4,    3071, 5820, 1,    3000, 5820,
         5,    94,   628,  1,    3000, 5826, 1,    6,    640,  8,    640,  5830,
         8,    640,  644,  0,    7,    644,  8,    644,  5836, 628,  634,  959,
         1,    628,  640,  283,  628,  634,  283,  634,  636,  1,    6,    590,
         1,    40,   160,  1,    266,  614,  1,    6,    178,  1,    8,    482,
         1,    8,    474,  4,    8,    61,   1,    6,    5860, 1,    6,    154,
         1,    8,    492,  1,    266,  656,  1,    2,    94,   4,    664,  5871,
         1,    3448, 5872, 0,    4,    4733, 3,    102,  5876, 1,    2,    5878,
         4732, 5878, 5880, 2,    94,   3288, 664,  3088, 5885, 0,    2,    4733,
         2,    103,  5876, 102,  5889, 5890, 4,    927,  2984, 102,  2723, 5894,
         4,    628,  3742, 628,  1808, 5899, 0,    3,    3708, 4,    656,  3709,
         628,  5903, 5904, 6,    8,    657,  2,    658,  5908, 659,  1808, 5910,
         664,  3088, 3275, 664,  3088, 3709, 926,  2863, 3470, 1,    8,    5332,
         9,    926,  5920, 7,    926,  3274, 5,    8,    5924, 9,    926,  5926,
         5,    926,  3274, 7,    8,    5930, 9,    926,  5932, 2,    905,  926,
         1,    8,    5936, 9,    926,  5938, 5,    6,    3208, 0,    7,    5942,
         1,    926,  5944, 2,    7,    926,  4,    9,    5948, 0,    5,    5950,
         1,    926,  5952, 6,    9,    3470, 0,    7,    5956, 1,    926,  5958,
         9,    926,  3470, 0,    7,    5962, 1,    926,  5964, 9,    926,  5948,
         0,    5,    5968, 1,    926,  5970, 0,    10,   267,  6,    8,    5975,
         10,   441,  5976, 7,    10,   828,  8,    826,  5980, 9,    828,  5982,
         7,    10,   836,  8,    834,  5986, 9,    836,  5988, 6,    191,  358,
         1,    8,    5992, 787,  5992, 5994, 4,    146,  191,  1,    8,    5998,
         807,  5998, 6000, 0,    201,  806,  1,    8,    6004, 807,  6004, 6006,
         0,    201,  786,  1,    8,    6010, 787,  6010, 6012, 0,    8,    2083,
         9,    1112, 2082, 1,    6016, 6018, 0,    8,    787,  788,  2162, 6022,
         3,    10,   376,  6,    8,    6027, 2,    48,   267,  6,    8,    6031,
         4,    267,  376,  6,    8,    6035, 1,    630,  5332, 4,    8,    5332,
         3,    6,    6040, 1,    5332, 6042, 630,  905,  3996, 8,    358,  376,
         3,    490,  6048, 3,    6,    1916, 8,    500,  6052, 1,    1916, 6054,
         3,    6,    1730, 2,    501,  1730, 1,    6058, 6060, 6,    624,  3841,
         2,    356,  905,  6,    3841, 6066, 51,   3818, 3850, 51,   3944, 4646,
         2,    4,    1173, 6,    8,    6074, 0,    1172, 6077, 2,    4,    614,
         0,    7,    6080, 9,    614,  6082, 6,    383,  2842, 0,    383,  1172,
         8,    266,  2843, 6,    2842, 6091, 92,   383,  4552, 9,    614,  2842,
         267,  584,  2842, 6,    9,    2842, 267,  2842, 6100, 2,    310,  927,
         9,    354,  6104, 2,    7,    1540, 9,    5360, 6108, 9,    1544, 1638,
         1,    4,    1544, 2,    5,    6114, 9,    1544, 6116, 2,    7,    4158,
         9,    1158, 6120, 0,    7,    1514, 9,    1638, 6124, 2,    8,    49,
         0,    3,    6128, 7,    48,   6130, 9,    6128, 6132, 2,    357,  1030,
         3,    312,  6136, 0,    93,   1030, 1,    312,  6140, 0,    217,  6136,
         1,    6,    2842, 2,    4,    6147, 8,    2843, 6148, 0,    7,    3708,
         8,    3008, 6153, 8,    2843, 6074, 0,    7,    1172, 8,    6074, 6159,
         8,    2843, 3008, 5,    6,    1644, 4,    383,  6164, 1,    2,    582,
         0,    383,  6168, 0,    383,  432,  2,    4,    394,  6,    8,    6174,
         10,   394,  6177, 376,  378,  389,  0,    2,    583,  383,  582,  6182,
         60,   383,  1876, 0,    2,    2333, 6,    8,    6188, 4,    2332, 6191,
         4,    1964, 1969, 383,  500,  1644, 0,    3,    92,   4,    6,    6199,
         8,    92,   6201, 8,    93,   6200, 9,    6202, 6204, 2,    491,  1312,
         3,    1568, 6208, 6,    133,  354,  0,    132,  6213, 3,    1568, 6214,
         0,    132,  747,  3,    1568, 6218, 4,    8,    354,  0,    7,    6222,
         3,    4,    6224, 5,    6,    6222, 355,  6226, 6228, 0,    7,    660,
         3,    4,    6232, 355,  5368, 6234, 3,    4,    1160, 355,  1574, 6238,
         1,    92,   628,  0,    3,    6242, 4,    6,    6245, 8,    6243, 6246,
         2,    8,    3935, 3,    1568, 6250, 3,    4,    490,  2,    8,    6255,
         3,    1568, 6256, 8,    282,  358,  2,    4,    6261, 8,    6261, 6262,
         6,    9,    432,  61,   660,  6266, 4,    146,  232,  4,    132,  6271,
         2,    8,    2743, 3,    290,  6274, 2,    6,    232,  4,    8,    6279,
         5,    290,  6280, 233,  660,  6274, 233,  2356, 6274, 1,    6,    2038,
         61,   660,  6288, 61,   644,  660,  61,   644,  5398, 41,   282,  358,
         7,    1886, 5762, 7,    60,   5762, 2,    5,    1886, 7,    1886, 6302,
         5,    358,  1886, 3,    358,  5762, 282,  358,  1259, 2,    41,   1886,
         4,    41,   5762, 8,    50,   358,  8,    40,   6317, 2,    51,   132,
         3,    40,   6320, 4,    51,   660,  5,    40,   6324, 4,    283,  660,
         5,    40,   6328, 2,    102,  283,  3,    40,   6332, 4,    94,   283,
         5,    40,   6336, 2,    5368, 6324, 2,    5368, 6328, 3,    4,    2954,
         2,    5,    2954, 6,    6344, 6346, 2,    5,    6344, 6,    6344, 6350,
         2,    7,    218,  233,  660,  6354, 3,    6,    218,  283,  634,  6358,
         0,    383,  5852, 0,    267,  5848, 9,    590,  6364, 0,    7,    5852,
         9,    614,  6368, 8,    266,  383,  0,    7,    6372, 6,    383,  6374,
         0,    6,    6373, 383,  6372, 6378, 1,    8,    584,  0,    267,  6382,
         7,    584,  6384, 0,    9,    5852, 7,    614,  6388, 0,    6,    591,
         383,  590,  6392, 0,    7,    6382, 267,  584,  6396, 0,    9,    5848,
         267,  590,  6400, 0,    5,    664,  4,    217,  6404, 358,  6404, 6406,
         3,    312,  500,  2,    7,    6410, 218,  6410, 6412, 9,    354,  500,
         2,    7,    6416, 218,  6416, 6418, 5,    302,  664,  4,    7,    6422,
         217,  6422, 6424, 7,    218,  228,  2,    9,    6428, 228,  6428, 6430,
         1,    38,   664,  0,    9,    6434, 41,   6434, 6436, 7,    218,  1124,
         2,    5168, 6440, 3,    4,    218,  7,    218,  6444, 9,    500,  6444,
         2,    6446, 6448, 7,    60,   218,  2,    9,    6452, 500,  6452, 6454,
         2,    9,    6446, 500,  6446, 6458, 146,  629,  6198, 146,  629,  3526,
         1,    2,    356,  41,   282,  6466, 5,    8,    216,  146,  232,  6471,
         146,  232,  3383, 2,    8,    11,   146,  232,  6477, 0,    8,    49,
         146,  232,  6481, 2,    4,    615,  7,    266,  614,  8,    6484, 6487,
         6,    8,    6484, 267,  6484, 6490, 267,  382,  3008, 267,  3008, 3012,
         6,    5518, 5532, 6,    8,    5518, 267,  5518, 6500, 6,    585,  5518,
         267,  382,  5518, 8,    591,  6484, 2,    6,    219,  3,    8,    6510,
         501,  6510, 6512, 3,    3106, 6510, 2,    218,  3107, 6,    3106, 6519,
         8,    505,  6510, 501,  3130, 6510, 3,    6,    3106, 219,  3106, 6526,
         219,  3106, 6358, 0,    5,    504,  2,    6,    6533, 8,    505,  6534,
         6,    221,  3106, 1,    4,    220,  2,    8,    6541, 6,    221,  6542,
         0,    9,    3698, 3,    242,  6546, 3699, 6546, 6548, 9,    660,  1188,
         310,  5368, 6552, 9,    356,  656,  40,   660,  6557, 4,    8,    2853,
         359,  5518, 6560, 9,    266,  6560, 359,  6560, 6564, 6,    635,  3288,
         8,    665,  3288, 6,    6569, 6570, 1,    6,    302,  660,  6354, 6574,
         6,    266,  310,  93,   706,  6578, 310,  640,  3174, 310,  640,  1578,
         6,    555,  634,  147,  2924, 6586, 9,    2102, 2156, 0,    41,   6590,
         41,   134,  6140, 0,    5,    26,   0,    8,    11,   3,    26,   6598,
         7,    6596, 6600, 0,    3,    26,   5,    26,   6598, 7,    6604, 6606,
         0,    3,    2162, 5,    1090, 2162, 7,    6610, 6612, 3,    1090, 2162,
         7,    4564, 6616, 19,   132,  6604, 8,    10,   19,   0,    3,    6622,
         19,   146,  6624, 2,    4,    94,   10,   94,   665,  0,    6629, 6630,
         10,   656,  665,  0,    3709, 6634, 0,    2,    95,   94,   3005, 6638,
         7,    8,    2984, 8,    2984, 6643, 6,    6642, 6645, 2,    9,    3742,
         5,    656,  3742, 7,    6648, 6650, 0,    9,    5870, 5,    94,   5870,
         7,    6654, 6656, 0,    2,    615,  383,  614,  6660, 267,  590,  5802,
         7,    8,    5802, 267,  5802, 6666, 6,    9,    2984, 2985, 6642, 6670,
         7,    8,    6670, 2985, 6670, 6674, 7,    8,    1188, 267,  584,  6678,
         41,   3930, 3944, 0,    3,    520,  5,    358,  6684, 8,    520,  6686,
         41,   196,  432,  0,    3,    1146, 7,    146,  6692, 8,    1146, 6694,
         0,    7,    1146, 3,    146,  6698, 8,    1146, 6700, 0,    7,    432,
         5,    60,   6704, 8,    432,  6706, 0,    5,    432,  7,    60,   6710,
         8,    432,  6712, 0,    5,    520,  3,    358,  6716, 8,    520,  6718,
         0,    203,  432,  60,   203,  1876, 0,    3,    358,  656,  3167, 6726,
         26,   157,  3944, 0,    10,   283,  2,    6,    661,  3,    6732, 6734,
         4,    282,  2869, 0,    2870, 6739, 4,    9,    94,   1,    2,    6742,
         4,    282,  6743, 0,    6744, 6747, 1,    2,    2898, 4,    282,  2899,
         0,    6750, 6753, 0,    3,    2898, 2,    6753, 6756, 0,    3,    6742,
         2,    6747, 6760, 0,    2,    12,   5,    6,    6764, 12,   133,  6766,
         7,    8,    2870, 5,    2868, 6770, 0,    2870, 6772, 7,    8,    6744,
         5,    6742, 6776, 0,    6744, 6778, 8,    926,  2722, 926,  4662, 6783,
         9,    926,  2722, 8,    6783, 6786, 2,    9,    4078, 2,    8,    4078,
         8,    6790, 6793, 2,    8,    4079, 3,    6790, 6796, 3,    8,    6790,
         4079, 6790, 6800, 4078, 6793, 6796, 0,    9,    3274, 1,    8,    6806,
         3275, 6806, 6808, 2723, 4662, 6786, 9,    926,  4662, 2723, 4662, 6814,
         2,    218,  283,  6,    218,  661,  6,    6818, 6821, 0,    2,    4801,
         1,    6,    6824, 92,   4800, 6825, 8,    6826, 6829, 0,    5,    5480,
         3,    6,    6832, 634,  5480, 6834, 2,    8,    283,  0,    5,    6838,
         3,    6,    6840, 634,  6838, 6842, 0,    5,    5474, 3,    6,    6846,
         634,  5474, 6848, 0,    5,    2954, 3,    6,    6852, 634,  2954, 6854,
         4,    9,    358,  0,    2,    6858, 8,    675,  6858, 359,  6860, 6862,
         6,    8,    6829, 1,    6824, 6866, 5,    8,    282,  1,    6,    6870,
         0,    3,    6872, 2,    6,    6871, 283,  6874, 6876, 0,    7,    6510,
         6,    218,  660,  1,    6880, 6882, 242,  302,  2041, 2,    8,    4675,
         2,    9,    4674, 665,  6888, 6890, 0,    8,    2471, 0,    9,    2470,
         629,  6894, 6896, 9,    664,  4674, 665,  6888, 6900, 9,    628,  2470,
         629,  6894, 6904, 6,    8,    1188, 132,  302,  6909, 132,  302,  2629,
         132,  302,  5787, 8,    1770, 3955, 6,    48,   94,   94,   1770, 6919,
         2,    232,  500,  8,    290,  6923, 4,    93,   1188, 8,    2843, 6926,
         2,    500,  635,  8,    644,  6931, 233,  660,  3910, 233,  660,  3106,
         4,    233,  1188, 8,    235,  6938, 4,    6,    219,  660,  6510, 6943,
         223,  660,  6354, 132,  226,  1677, 4,    6,    218,  132,  221,  6950,
         48,   146,  629,  10,   41,   282,  60,   376,  629,  267,  282,  358,
         6,    242,  635,  9,    232,  6962, 9,    146,  1188, 232,  1189, 6966,
         282,  291,  2734, 8,    41,   746,  282,  747,  6972, 2,    7,    656,
         8,    40,   6977, 0,    656,  6979, 8,    146,  1189, 7,    282,  6982,
         6,    216,  661,  217,  232,  6986, 9,    232,  6982, 8,    1189, 5762,
         7,    282,  6992, 0,    7,    6982, 9,    6982, 6996, 1,    6,    6926,
         8,    6926, 7000, 0,    3,    634,  7,    634,  7004, 6,    283,  7006,
         1,    628,  7006, 6,    283,  634,  283,  7004, 7012, 2,    7,    282,
         0,    6,    7017, 4,    9,    7016, 283,  7018, 7020, 0,    51,   634,
         1,    628,  7024, 1,    628,  6926, 8,    644,  7024, 2,    7,    628,
         233,  660,  7032, 0,    3,    7012, 283,  7012, 7036, 4,    41,   232,
         1,    2,    7040, 8,    40,   7043, 6,    7040, 7045, 7,    266,  310,
         6,    266,  311,  0,    9,    7050, 267,  7048, 7052, 7,    242,  634,
         242,  282,  635,  243,  7056, 7058, 7,    60,   6870, 282,  747,  7062,
         7,    1886, 6870, 282,  747,  7066, 7,    1886, 2558, 282,  747,  7070,
         7,    60,   2558, 282,  747,  7074, 267,  2652, 2654, 1,    6,    7078,
         7,    2654, 7080, 5,    266,  282,  6,    267,  310,  7,    7084, 7086,
         1,    8,    48,   0,    6,    7091, 0,    475,  7090, 1,    7092, 7094,
         6,    8,    242,  6,    242,  634,  8,    7099, 7100, 4,    1188, 3887,
         6,    2954, 7104, 6,    8,    146,  0,    2,    7109, 0,    9,    7108,
         6,    7110, 7113, 0,    9,    4800, 6,    6824, 7117, 3,    634,  1188,
         6,    2954, 7120, 6,    634,  7005, 8,    7006, 7124, 6,    9,    7004,
         6,    7006, 7129, 6,    2954, 6926, 6,    5480, 7024, 9,    1188, 3874,
         6,    2954, 7136, 6,    242,  266,  242,  282,  7141, 9,    656,  2760,
         7,    376,  3742, 9,    656,  7146, 1,    94,   146,  0,    7,    7150,
         9,    7150, 7152, 0,    41,   972,  9,    656,  7156, 0,    41,   6976,
         9,    656,  7160, 0,    94,   147,  146,  629,  7164, 6,    242,  267,
         0,    7,    7168, 9,    7168, 7170, 0,    95,   146,  94,   629,  7174,
         6,    8,    7151, 0,    7150, 7179, 0,    41,   656,  7,    40,   656,
         9,    7182, 7184, 0,    8,    475,  9,    5858, 7188, 0,    9,    424,
         0,    8,    425,  1,    7192, 7194, 1,    40,   232,  9,    298,  7198,
         1,    6,    200,  7,    40,   200,  9,    7202, 7204, 268,  614,  629,
         0,    9,    2466, 6,    8,    2467, 629,  7210, 7212, 0,    9,    492,
         493,  5866, 7216, 1,    8,    7216, 493,  7216, 7220, 0,    8,    267,
         584,  629,  7224, 6,    675,  3096, 8,    406,  1091, 1,    406,  3096,
         8,    1172, 4552, 8,    406,  520,  6,    523,  3096, 358,  406,  523,
         92,   253,  4552, 1,    2546, 3818, 359,  520,  3096, 0,    656,  5909,
         0,    629,  656,  8,    282,  629,  6,    232,  629,  9,    232,  656,
         0,    2,    4732, 4,    102,  7258, 4732, 5888, 7261, 2,    926,  3275,
         6,    1030, 7264, 0,    3274, 7267, 6,    1030, 3402, 0,    3274, 7271,
         4,    102,  3402, 0,    3274, 7275, 8,    40,   3402, 0,    3274, 7279,
         8,    554,  3402, 0,    3274, 7283, 2,    4078, 7283, 2,    4078, 7279,
         2,    4078, 7271, 2,    4078, 7275, 6,    721,  1484, 38,   664,  1189,
         6,    572,  608,  50,   135,  500,  491,  500,  664,  40,   94,   1603,
         61,   94,   1568, 4,    6,    1835, 61,   94,   7308, 0,    8,    146,
         2,    6,    7313, 102,  147,  7314, 359,  972,  1568, 2,    6,    200,
         40,   102,  7321, 2,    5,    1602, 2,    8,    1603, 6,    7325, 7326,
         4,    6,    200,  40,   94,   7331, 3,    4,    972,  4,    354,  973,
         6,    7334, 7337, 8,    92,   644,  92,   5388, 7341, 2,    132,  645,
         2,    133,  644,  3,    7344, 7346, 5,    644,  660,  4,    645,  660,
         661,  7350, 7352, 3,    132,  644,  133,  7344, 7356, 2,    645,  7356,
         133,  7356, 7360, 4,    645,  7350, 661,  7350, 7364, 8,    92,   645,
         9,    5388, 7368, 4,    644,  661,  5,    7352, 7372, 2,    9,    50,
         5,    6,    7376, 8,    3309, 7378, 51,   2454, 7378, 4,    8,    7378,
         51,   7378, 7384, 4,    7,    7376, 6,    2429, 7388, 4,    2429, 7378,
         2,    9,    2454, 5,    6,    7394, 51,   2454, 7396, 4,    6,    7377,
         2429, 7376, 7400, 6,    132,  660,  5,    40,   660,  3,    4,    132,
         6,    132,  7408, 8,    40,   359,  8,    40,   93,   2,    359,  660,
         6,    61,   660,  8,    359,  634,  5,    8,    290,  290,  2356, 7422,
         8,    232,  290,  3,    4,    7426, 5,    290,  7428, 5,    232,  290,
         2,    8,    7432, 3,    290,  7434, 2,    5,    7426, 3,    290,  7438,
         290,  2360, 7422, 4,    8,    2360, 5,    290,  7444, 4,    232,  660,
         2,    5,    7448, 233,  7448, 7450, 2,    132,  232,  3,    4,    7454,
         233,  7454, 7456, 4,    232,  661,  2,    7448, 7461, 2,    133,  232,
         4,    7454, 7465}};
};

} /* namespace mockturtle */
